Formally Verified Resource Bounds through Implicit Computational Complexity
summary
Proposes a mechanically checked soundness proof that completing an mwp flow analysis derivation implies polynomial bounds on variable growth, formalizes a small imperative language and the mwp semi‑ring, and plans a Coq proof development to verify the original Jones–Christensen theorems; notes practical nondeterminism that makes the original analysis fail on exponential cases and points to an existing Python prototype pi mwp and to mwp flow analysis as the concrete technique under formalization.
AI-written summary · about
chapters (9)
- 0:00Correctness and resource bounds
- 1:04Resource bounds matter
- 2:53Implicit computational complexity
- 4:37mwp flow analysis example
- 9:14mwp guarantees polynomial bounds
- 10:41Formal verification with theorem provers
- 12:49Formalizing mwp analysis
- 15:37Verified complexity applications
- 17:24Q&A on static analyzers