Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
summary
Introduces Trillium as a language-agnostic separation-logic framework that proves intensional refinements between program traces and labeled transition models, using a fuel-based simulation to bridge Iris-style step-indexed reasoning to liveness. Instantiates with Fairis to prove fair termination of concurrent programs under fair scheduling by refining to well-founded models, and with Aneris to relate distributed implementations to TLA+ specifications; artifacts and mechanized proofs are available.
AI-written summary · about
chapters (7)
- 0:00Trillium introduction
- 2:37Fair termination in concurrency
- 5:44Transition systems modeling
- 8:55Feris and Aneris instantiations
- 10:20Proving fair termination
- 13:51Refinement relation
- 14:38Q&A
related talks
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
21mA Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
28mDependent Session Protocols in Separation Logic from First Principles
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic