Commutativity Simplifies Proofs of Parameterized Programs
summary
Extends commutativity-based reductions to parameterized programs and encodes each reduction by transforming the thread template into another parameterized program so existing verifiers apply; implements a pipeline that translates the result to constrained Horn clauses and runs an off-the-shelf CHC solver. On 19 benchmarks the original pipeline proves 4, reports “no thread-modular proof” for 11 and times out on 4; with lexicographical reductions it proves 14, finds none impossible, and still has a few solver timeouts mitigated by a symmetry-reduction optimization.
AI-written summary · about
chapters (9)
- 0:00Commutativity in verification
- 2:08Parameterized programs
- 4:55Ghost state limitations
- 7:25Commutativity simplifies proofs
- 9:10Reduction to execution traces
- 10:57Automating verification reductions
- 12:21Experimental results
- 13:24Contributions and insights
- 14:28Q&A
related talks
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
19mScenario-based Proofs for Concurrent Objects
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
23mTermination Analysis for the pi-Calculus by Reduction to Sequential Program Termination
22mContext-Bounded Verification of Thread Pools
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
25mParametrised Verification of Intel-x86 Programs