Automated Expected Value Analysis of Recursive Programs
summary
Defines infer[.], a term representation that translates weakest pre-expectation semantics for recursive, imperative probabilistic programs into first-order constraints solvable by SMT, using logical variables to encode procedure summaries and continuations. Prototype ev-imp implements the pipeline, automatically handling non-tail recursion and recovering exact closed-form bounds on examples (e.g. occupancy/balls bounds). Evaluation covers 53 benchmarks, 94% solved fully automatically, full suite running in about five minutes.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:05Ball throwing example
- 2:31Tool demo and contributions
- 3:58Language semantics
- 5:43Sampling and recursion
- 7:50Automating recursion challenges
- 9:14Expectation transformer templates
- 10:41Evaluation and related work
- 12:26Benchmark results
- 13:40Q&A
related talks
15mRaising Expectations: Automating Expected Cost Analysis with Types
15mA Modular Cost Analysis for Probabilistic Programs
30mRelatively Complete Verification of Probabilistic Programs
39mA Reusable Machine-Calculus for Automated Resource Analyses
19mCompiling Probabilistic Programs for Variable Elimination with Information Flow
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
29mEfficient Evaluation with Controlled Definition Unfolding
30mAnalyzing Programs with SMT Solvers