Mechanizing the CMP Abstraction for Parameterized Verification
summary
Provides a machine-checked formalization of the CMP abstraction with syntax-directed abstraction and strengthening rules proven sound in Isabelle/HOL, implements an automated tool AutoCMP that generates Isabelle proof scripts while running model checking, applies the workflow to several parameterized protocols including the Stanford FLASH cache protocol and discovers two inaccuracies in prior manual CMP uses, proves symmetry reduction and assume-guarantee lemmas, and integrates abstraction, strengthening and proof generation successfully on industrial-scale examples.
AI-written summary · about
chapters (8)
- 0:00Mechanized CMP abstraction
- 3:00CMP formalization challenges
- 7:09Symmetry in parameterized protocols
- 10:28Guarded abstraction principles
- 13:33Syntax-guided abstraction
- 17:33Tool implementation and cases
- 19:03Conclusion and future work
- 19:45Q&A
related talks
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
15mStructural Abstraction and Refinement for Probabilistic Programs
15mStatically Verified Refinements for Multiparty Protocols
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
21mTowards composable proofs of cache coherence protocols
13mCharacterizing Implementability of Global Protocols with Infinite States and Data