Quantitative Bounds on Resource Usage of Probabilistic Programs
summary
Extends cost supermartingales to yield sound expectation bounds for programs with positive and negative costs and unbounded updates provided a lower bounded total cost holds, combines those martingales with stochastic invariants to get tail bounds even when expected cost is infinite, automates synthesis via template-based synthesis that reduces to existential polynomial constraints solved by SMT (algorithm runtime in PSPACE), provides a prototype that solves examples previous methods cannot and runs in seconds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:02Cost analysis
- 3:51Limitations of cost analysis
- 5:34Contributions and proof rules
- 6:58Expectation bounds with supermartingales
- 10:27Tail bounds with invariance
- 12:32Automation and implementation
- 15:42Evaluation and results
- 16:04Conclusion and future work
- 16:53Q&A
related talks
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
15mStructural Abstraction and Refinement for Probabilistic Programs
20mThe Complexity of Infinite-Horizon General-Sum Stochastic Games
27mParameterized Infinite-State Reactive Synthesis
25mStep-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
15mCAMP: Cost-Aware Multiparty Session Protocols
35mApproximation hardness and online algorithms for resource scheduling
01h 02mDerandomization to Boolean Circuit Lower Bounds