Unified Compositional Formal Methods: Exact Separation Logic and the Gi...
summary
Claims a single exact separation logic (ESL) that is sound for both over‑approximate verification and under‑approximate bug finding, formalizes an internalization mechanism to handle function calls in under‑approximate settings, and proves compositional rules and soundness. Implements a unified compositional symbolic executor as the Gillian unified platform, and demonstrates it on reusable library specs (singly linked lists and balanced trees), showing the list‑length proof works and explaining loop termination must be enforced for ESL to hold.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:03ESL program logic
- 2:46Motivation for exact SL
- 5:15Function calls in under-approx SL
- 8:53Obstruction in under-approx SL
- 14:34Approximation-free logic
- 18:11ESL logic and examples
- 18:32Q&A
related talks
22mbabble: Learning Better Abstractions with E-Graphs and Anti-unification
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
29mType Inference Techniques: Implementation and Formalization, Better Together
21mPractical compositional diagramming
01h 10mMedium-scale automation for proof assistants
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
16mThe Modular Imperative: Rethinking LLMs for Maintainable Software
15mCorrectness-by-Construction for Feature-Oriented Software Product Lines