U-turn: Forward-driven backward analysis for incorrectness
summary
Combines forward IL to produce only true reachable errors with a backward SIL proof that extracts the actual preconditions responsible for those errors, producing P' ⊆ P by replaying the IL proof tree. Implements a proof system in a new UT format that inductively walks command structure and incorrectness proofs; example reproduces an array-length bug and narrows the cause to L == 2. Prototype works on examples and is adaptable to other analyses.
AI-written summary · about
chapters (14)
- 0:00U-turn analysis intro
- 0:22Correctness vs incorrectness
- 1:45Collecting semantics & weakest PT
- 3:56Incorrectness logic taxonomy
- 5:00Forward logic rules
- 6:31False postconditions & path drops
- 6:54Backward logic rules
- 8:01Combining forward & backward
- 9:45Combined proof system details
- 11:29Path rules in combined system
- 12:55Faulty array init case study
- 13:59Precondition inference for errors
- 14:21Dualizing approach & future work
- 15:28Conclusion & benefits