Formal Foundations for Translational Separation Logic Verifiers

on YouTube ↗21m

" summary

Provides a formal, mechanized framework that proves soundness of translational separation-logic verifiers by defining a core IVL with both operational and axiomatic semantics, using Isabelle/HOL proofs. Key technical moves: a generalized separation algebra unifying separation logic and implicit dynamic frames, angelic non-determinism to model backend choices, and a proof-reconstruction technique to turn IVL derivations into separation-logic proofs. Instantiates to Viper, connects to symbolic-execution and VCG back-ends, and ships reusable artifacts.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 1:05Separation logic in verifiers
3. 3:57Encoding assertions in IVL
4. 6:03Soundness goal
5. 7:07Challenges in semantics
6. 8:10Core IVL design
7. 10:19Dual semantics
8. 11:21Operational semantics independence
9. 12:25Angelic nondeterminism
10. 14:33Contributions and formalization
11. 15:54Practical instantiation
12. 16:14Q&A