The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
summary
Converts interleaving-based certificates produced by Ultimate Automizer into compact Owicki–Gries thread-modular proofs by synthesizing ghost variables tracking empire state and building a finite-state “empire” abstraction that groups places into territories. Evaluated on 1,100 SV-COMP C programs, proof generation is about 119× faster, resulting proofs are ~15× smaller and validation runs ~26× faster than a naive-location-encoding baseline, producing checkable certificates that significantly reduce interleaving blowup.
AI-written summary · about
chapters (10)
- 0:00Ghost-based modular proofs
- 3:20Threat-modular proofs and ghosts
- 7:12Petri programs and territories
- 9:22Computing empires from proofs
- 12:11Thread-modular proofs
- 14:19Evaluation vs naive approach
- 16:25Conclusion and future work
- 17:32Q&A: Completeness
- 18:13Q&A: Memory compatibility
- 19:20Q&A: Soundness of empires
related talks
32mCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
11mMorello Cerise: proving secure encapsulation (work in progress)
01h 05mVerifying Infinitely Many Programs at Once
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
15mModular Reasoning about Global Variables and Their Initialization