A New Perspective on Commutativity in Verification
summary
Argues that commutativity becomes a primary search dimension so verification can find an easier-to-prove program and carry results back soundly, formalizes this with Mazurkiewicz-style lexicographic reductions and looping tree automata, gives a linear-time subsumption check reducing to Horn satisfiability, and builds a tool that searches reductions plus proofs; on 1,200 benchmarks the search-enabled approach solves about 50 more problems and cuts overall time roughly in half, while adding contextual, semi‑, abstract and stratified commutativity.
AI-written summary · about
chapters (12)
- 0:00Introduction and background
- 1:04Commutativity and reductions
- 4:42Verification through reduction
- 8:55New paradigm for verification
- 12:17Operational proof framework
- 16:52Lexicographic reductions
- 20:41Contextual orders
- 23:42Automated proof construction
- 27:48Advanced commutativity models
- 31:28Stratified commutativity
- 35:44Future work and challenges
- 38:45Conclusion and Q&A
related talks
01h 16mVerifying, Inferring and Exploiting Code Commutativity
27mVeracity: Declarative Multicore Programming with Commutativity
15mClosing Remarks
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 05mVerifying Infinitely Many Programs at Once
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
19mAutomated Verification of Fundamental Algebraic Laws