Verified Symbolic Execution with Kripke Specification Monads…
summary
Presents a verified symbolic executor implemented as a Kripke-indexed symbolic specification monad that manipulates deeply embedded assertions, proves soundness by relating it via a Kripke logical relation to a shallow verification-condition interpreter, and instantiates axioms in Iris against an operational semantics. Ships as the Katamaran tool with artifacts available, supports user theories for SMT and separation logic, and reports verification performance often 1–2 orders of magnitude faster than comparable proof-mode approaches.
AI-written summary · about
chapters (12)
- 0:00Verified symbolic execution intro
- 1:14Metaprograms to deep embedding
- 3:37Shallow execution with monads
- 6:26Symbolic execution basics
- 8:47Symbolic values and constraints
- 10:25Symbolic execution challenges
- 12:48World semantics for constraints
- 14:43World-indexed types
- 16:37Kripke logical relations
- 17:01Katamaran verification
- 18:13Performance results
- 19:29Conclusion