Compositional Symbolic Execution for the Next 700 Memory Models
summary
Presents a mechanized formal foundation for memory-model‑parametric compositional symbolic execution, claiming soundness for both separation logic and incorrectness separation logic, implemented and proved in Rocq and inspired by Gillian. Foundations are parametric on concrete/resource/symbolic memory, with consume/produce operations and a machine-checked link from symbolic to concrete semantics. Instantiations include C and a CHERI capability model, with CHERI OX soundness taking about 19,000 lines of proofs; UX soundness remains work in progress.
AI-written summary · about
chapters (10)
- 0:00Compositional symbolic execution
- 2:13Formal foundations
- 4:41CSSE theory
- 5:24CSSE engine overview
- 6:27Memory model structure
- 8:15Soundness theorem
- 8:57Proving engine soundness
- 10:48Function call semantics
- 12:36Memory model instantiation
- 13:43Future work
related talks
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
22mCategorical Semantics of Probabilistic Symbolic Execution
19mWhat Compilers desire from Weak Memory Semantics
17mA Formally Verified Foundation for Compositional Heterogeneous Coherence
23mVerified Compilation of C Programs with a Nominal Memory Model
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
19mCHERI C semantics