STandV 2026 @ Vrije Universiteit Brussel

Lecture 1: Separation Logic and The Gillian Platform

• An introduction to Separation Logic, a modern Hoare logic
• Core Compositional Symbolic Execution
• A Gillian Taster

Exercises

• Simple assertions
• List concatenation

Resources

• Lecture slides
• Separation Logic proof rules
• Gillian taster video

References

• Separation Logic: A Logic for Shared Mutable Data Structures (John Reynolds, LICS 2002)
• Incorrectness logic (Peter O'Hearn, POPL 2020)
• Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic (Azalea Raad et. al., CAV 2020)
• Gillian: a Multi-language Platform for Compositional Symbolic Analysis (Philippa Gardner, Program Logic Seminar at Collège de France 2021)
• Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees (Nat Karmios et. al., TACAS 2025)

Lecture 2: Compositional Symbolic Execution

• Compositional symbolic execution, parametric on the state
• Semi-automatic verification of function specifications
• Tools for semi-automatic verification and true bug finding
• An introduction to the Gillian Platform

Resources

• Lecture slides
• Gillian-While demo
• Gillian-C demo

References

• Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Andreas Lööw et. al., ECOOP 2024)
• Compositional Symbolic Execution for the Next 700 Memory Models (Andreas Lööw et. al., OOPSLA 2025)