Specifying and Verifying Future Conditions
summary
Proposes over-approximating Hoare-style forward rules that embed future-condition obligations into program states so each event is processed once, plus a bag of future conditions predicate to model loops and recursive allocations. Formal soundness appears proved in Coq. Evaluation on ~1,600 LOC uses 34 handwritten API specs, infers ~100 function specs and ~20 loop invariants, expects 51 violations and reports 55. Claims linear trace processing, no false negatives, and detects real-world API misuses (e.g., use-after-free, leaked heap arrays).
AI-written summary · about
chapters (16)
- 0:00Future conditions verification
- 0:22Research project overview
- 1:05Future conditions and specs
- 3:14Prior work limitations
- 3:36Detecting use-after-free bugs
- 5:22Function calls and constraints
- 6:45Inefficiency in prior checks
- 7:07Embedding conditions in states
- 9:17Loops with recursive predicates
- 10:41Loop invariants for resources
- 12:04Verification system soundness
- 14:13Instrumented semantics
- 16:46Experimental results
- 18:31Comparison and trade-offs
- 19:56Future work challenges
- 20:37Q&A
related talks
01h 05mVerifying Infinitely Many Programs at Once
20mOn Extending Incorrectness Logic with Backwards Reasoning
22mExecution Time Program Verification With Tight Bounds
28mGradual Verification: Assuring Software Incrementally
27mUnrealizability Logic
15mGradual Verification of Recursive Heap Data Structures
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
12mFO-Complete Program Verification for Heap Logics