A Modular Cost Analysis for Probabilistic Programs
summary
Presents a modular method that derives symbolic upper bounds on expected resource cost for probabilistic imperative programs by combining the ERT-calculus with a lightweight value analysis, constraint templates over base functions, Positivstellensatz (Handleman) reduction and off‑the‑shelf SMT solving (example yields k = 2 for the biased random walk). Implements the approach in eco-imp, proves soundness against a new operational semantics, and beats prior tools on benchmarks (trader, coupon collector, NEST), often achieving two orders of magnitude faster runtime.
AI-written summary · about
chapters (11)
- 0:00Static Resource Analysis
- 0:28Conventional vs Probabilistic Programs
- 1:38Example: Random walk
- 2:19State of the Art in Automated Analysis
- 4:17Probabilistic GCL
- 5:10The ERT Calculus inspired by Dijkstra's weakest precondition transformer
- 5:59The ECT-Calculus Theorem Correctness
- 7:32Automation
- 10:23Experimental Evaluation
- 13:46Nested Loops
- 14:23Conclusion
related talks
15mRaising Expectations: Automating Expected Cost Analysis with Types
17mAutomated Expected Value Analysis of Recursive Programs
17mModular Verification of Probabilistic Constant-Time
39mA Reusable Machine-Calculus for Automated Resource Analyses
23mA Cost-Aware Logical Framework
18mEquivalence and Similarity Refutation for Probabilistic Programs
25mA Modular Static Cost Analysis for GPU Warp-Level Parallelism
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis