OPLSS 2026 @ University of Oregon

Lecture 1: Separation Logic

• An introduction to Separation Logic, a modern Hoare logic
• The specification and verification of heap-manipulating programs
• Tools for verification and true bug detection, based on compositional symbolic execution

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)

Lecture 2: From Separation Logic to Compositional Symbolic Execution

• Experience with Separation Logic
• Core Compositional Symbolic Execution
• Automatic whole-program symbolic analysis and bug detection

Exercises

• Collections-C singly-linked lists

Resources

• Lecture slides

References

• Incorrectness logic (Peter O'Hearn, POPL 2020)
• Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic (Azalea Raad et. al., CAV 2020)
• Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Andreas Lööw et. al., ECOOP 2024)

Lecture 3: Compositional Symbolic Execution

• Compositional symbolic execution, parametric on the state
• Semi-automatic verification of function specifications

Resources

• Lecture slides

References

• Compositional Symbolic Execution for the Next 700 Memory Models (Andreas Lööw et. al., OOPSLA 2025)

Lecture 4: Semi-automatic Verification and Automatic Bug Detection

• An introduction to the Gillian platform
• Gillian-While with simple block-offset memory model
• Gillian-C with full-scale C memory

Resources

• Lecture slides
• The Gillian lab

References

• [Lecture] 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)