U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
summary
Combines forward Incorrectness Logic derivations with backward Sufficient Incorrectness Logic by instrumenting backward proof rules with the forward derivation tree, producing a deterministic proof strategy that eliminates proof-search nondeterminism (e.g., loop unrolling uses the exact unroll count seen forward: 5 vs 2). Demonstrates handling pointer-aliasing in a model of vector::push_back so the backward run only explores the aliased case. Claims a rule format for inter-analysis instrumentation and proves a progress theorem giving an algorithm that computes a refined precondition forward derivation as guide.
AI-written summary · about
chapters (14)
- 0:00Incorrectness analysis intro
- 0:21Defining incorrectness analysis
- 1:46Forward vs backward analysis
- 3:09Challenges in backward analysis
- 5:14Nondeterminism in programs vs proofs
- 7:21Introducing U-turn approach
- 9:04U-turn transforms derivations
- 10:31U-turn loop unrolling example
- 11:53U-turn with C++ push_back
- 16:05U-turn judgment details
- 17:54Progress theorem guarantees
- 18:59Bidirectional logic guidance
- 20:01Conclusion and future work
- 20:21Q&A
related talks
20mOn Extending Incorrectness Logic with Backwards Reasoning
13mRevealing Sources of (Memory) Errors via Backward Analysis
26mAutomatic Rollback Suggestions for Incremental Datalog Evaluation
13mBackward Symbolic Execution with Loop Folding
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
20mFormal framework for reasoning about the precision of dynamic analysis
27mUnrealizability Logic
22mFrom FP to OOP and Back, Consistently