OPLSS 2026 @ University of Oregon
Note
These lectures took place at the Oregon Programming Languages Summer School at University of Oregon in June 2026.
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
Resources
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
Resources
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
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
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)