Automated Verification of Fundamental Algebraic Laws
summary
A verifier called Propel automatically conjectures and proves auxiliary lemmas (distributivity, generalizations) for a purely functional Scala subset, uses typing to derive induction hypotheses, and crucially tracks disequalities to prune useless branches. Implementation reasons about equalities and inequalities, performs one-level unfolding, and scores and selects proof branches. Evaluation versus five state-of-the-art provers on 142 instances shows Propel verifies more properties (and times out less) across domains like CRDTs and list/number benchmarks.
AI-written summary · about
chapters (9)
- 0:00Automated algebraic verification intro
- 1:45Automate algebraic law verification
- 2:28Tool demo for automatic verification
- 5:21Lemma generation strategies
- 7:50Proving addition commutativity
- 11:02Tracking disequalities insights
- 12:49Evaluation vs theorem provers
- 13:53Key insights and availability
- 14:36Conclusion
related talks
46mRefinement Types from Light to Deep Verification
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
19mVelvet: A Multi-Modal Verifier for Effectful Programs
01h 01mMulti-Modal Verification of Distributed Systems in Lean
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
47mYou Didn't Know It, but You Really Want to Learn Sequent Calculus
49mCompile-time Logic Programming in Scala: what for?
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers