Revealing Sources of (Memory) Errors via Backward Analysis
summary
Claims a new backward under‑approximation proof system called SIL and a memory‑aware specialization Separation SIL that are sound and (relatively) complete for locating error sources; gives a theorem that for any syntactic postcondition Q and atomic command C it computes a syntactic strongest SIL precondition P via an explicit algorithm; applies to pointers and dynamic allocation (example: vector push_back that may reallocate and invalidate a prior pointer); includes a proof‑of‑concept implementation (student project) validating the backward inference approach.
AI-written summary · about
chapters (7)
- 0:00Memory error analysis intro
- 1:47Limitations of existing logics
- 3:51Backward under-approximation
- 6:17Incorrectness logic proof
- 6:37Separation Seal for errors
- 10:32Conclusion and future work
- 11:38Q&A
related talks
20mOn Extending Incorrectness Logic with Backwards Reasoning
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction
59mUnder-approximation for Scalable Bug Detection
13mBackward Symbolic Execution with Loop Folding
21mEmbedding Hindsight Reasoning in Separation Logic
57mInvited Talk: Bridging Safety and Performance
19mPete's Footprints
20mAutomatic and Incremental Repair for Speculative Information Leaks