Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
summary
Built on Iris, Diaframe provides a foundational yet automated verifier for fine‑grained concurrency, using syntax‑directed rule versions, goal‑directed proof search and bi‑abduction to open invariants and handle atomic operations. It is extensible to custom ghost resources and aims for no global backtracking. Evaluation on 24 examples from the literature shows automation comparable to prior tools and replaces long manual proofs, yielding about a 90% proof-size reduction over plain Iris in their benchmarks.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:45Diaframe: approach
- 2:52Diaframe: evaluation
- 4:59Diaframe: key ideas
- 6:01Symbolic execution
- 6:54Fine-grained concurrency in Iris
- 8:42Fine-grained concurrency in Diaframe
- 9:58Proof search in Diaframe
- 12:47Questions?
related talks
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
23mWill it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage(…)
16mAutomated Verification of Parametric Channel-Based Process Communication
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
41mType-driven Development of Communicating Systems in Idris