On Extending Incorrectness Logic with Backwards Reasoning
summary
Extends incorrectness logic with underspecification so postconditions can ignore irrelevant variables, provides a backwards-proof system that produces presumptions, and formalizes soundness and completeness (for a defined subset) in Isabelle/HOL. Prototype uses SMT solvers to instantiate rules, leverages loop summaries (closed-form iteration effects) to find iteration counts, and runs on SV-COMP benchmarks where presumption sizes drop substantially; soundness checks fail below 100% when unsupported constructs (floats, unsummarizable vars) occur.
AI-written summary · about
chapters (11)
- 0:00Incorrectness logic intro
- 1:05Incorrectness vs Hoare logic
- 3:38Backwards reasoning in logic
- 6:09Extending logic with underspec
- 7:13Proof system for backwards
- 8:16Loops and SMT solvers
- 10:45Variable values zoom
- 13:08Loop invariance in proofs
- 14:13SV-COMP evaluation
- 16:23Future work
- 17:50Conclusion & Q&A
related talks
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction
23mSpecifying and Verifying Future Conditions
13mRevealing Sources of (Memory) Errors via Backward Analysis
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
27mUnrealizability Logic
14mA Hoare Logic For Symmetry Properties
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...