Execution Time Program Verification With Tight Bounds
summary
Proof system gives three Hoare-style logics with worst-case bounds, amortized potential method, and an exact-cost logic (language restricted: equal-cost branches and for-loops). Soundness is proved against an annotated cost-aware operational semantics. A VC generator/weakest-precondition produces obligations sent to Easycrypt and an OCaml prototype that validates examples: insertion sort proven O(n^2), binary search O(log n), binary counter amortized from n log n down to Θ(n), and a filter with exact linear cost. Toolchain and proofs are implemented and automated.
AI-written summary · about
chapters (7)
related talks
23mSpecifying and Verifying Future Conditions
27mUnrealizability Logic
12mFO-Complete Program Verification for Heap Logics
01h 05mVerifying Infinitely Many Programs at Once
14mA Hoare Logic For Symmetry Properties
21mExact Loop Bound Analysis
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mMechanised Hypersafety Proofs about Structured Data