Stratified Commutativity in Verification Algorithms for Concurrent Programs
summary
Defines a formal framework for abstract commutativity relations with a simple soundness condition and an automatic method to derive such relations from a partial proof, integrates that into an abstraction‑refinement verifier, and proves safety of the generated relations; introduces stratified commutativity, a proof rule and an algorithm that sequentially composes multiple incomparable relations (optimal combination proven), gives a decidable variant using a partial‑order‑reduction‑based decision procedure, and reports empirical improvements on concurrent verification benchmarks.
AI-written summary · about
chapters (10)
- 0:00Stratified commutativity intro
- 0:23Commutativity in concurrent programs
- 4:24Safe commutativity via abstraction
- 7:56Formalizing commutativity proofs
- 11:07Projection to proof abstraction
- 15:21Limitations of commutativity relations
- 16:23Stratified commutativity proof rule
- 19:58Decidable verification with orders
- 20:41Summary and contributions
- 21:22Q&A
related talks
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
19mScenario-based Proofs for Concurrent Objects
27mC4: verified transactional objects
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
19mCommutativity Simplifies Proofs of Parameterized Programs
20mVisibility Reasoning for Concurrent Snapshot Algorithms