Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
summary
Proposes consistency-preserving propagation that prevents self-loops in the ordering theory so consistency checking and conflict-clause generation become unnecessary, implemented as a prototype on top of CBMC + MiniSat and parameterized for SC, TSO and PSO. Preventive reasoning marks fragile literals and blocks assignments that would create cycles, reducing SMT decisions and propagations. Benchmarks (including comparisons to CBMC, CSeq and YOGAbmc) show the prototype solves more cases and uses less memory, demonstrating a measurable performance win.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:19The Problem
- 0:51Symbolic Encoding
- 2:31Ordering Consistency Theory
- 3:44Basic Theory Solver
- 4:13Consistency-Preserving Theory Solver
- 4:30Preventive Reasoning
- 5:36Evaluation
- 6:55Conclusions
related talks
17mA Formally Verified Foundation for Compositional Heterogeneous Coherence
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
15mTowards Proof Stability in SMT-based Program Verification
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
27mProducing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
15mSoundness of Predictive Concurrency Analyses
30mProof Logging for Constraint Programming