Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
summary
A prototype automatically synthesizes simultaneous potentials and anti-potentials as polynomial templates, translates the universal polynomial constraints via Handelman's theorem into a linear program, and solves/optimizes it to produce a numeric threshold t. It supports polynomial arithmetic and nondeterminism, computes tight thresholds for 14 of 19 benchmarks from the literature, and fails on five examples due to lack of disjunctive (piecewise) reasoning, which the authors identify as the main limitation.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:43Example
- 4:24Potential functions (PF)
- 5:35Anti-potential functions (anti-PF)
- 5:53PFs and anti-PFs for differential cost analysis
- 7:37Simultaneous PF and anti-PF synthesis
- 10:11Key features of our method
- 11:00Empirical Evaluation
- 12:43Conclusion
related talks
15mA Modular Cost Analysis for Probabilistic Programs
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
18mEquivalence and Similarity Refutation for Probabilistic Programs
23mGenerating Programs for Polynomial Multiplication with Correctness Assurance
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
16mTesting Differential Privacy with Dual Interpreters