Newtonian Program Analysis of Probabilistic Programs
summary
Presents NPA-PMA, an interprocedural framework that generalizes Newtonian Program Analysis to probabilistic, nondeterministic, and conditional branching by introducing ω-continuous pre-Markov algebras (ωPMAs) and encoding programs as regular infinite-tree expressions. Implements a syntactic linearization that makes Newton’s method applicable to tree equations with three confluent operations, builds a solver pipeline that computes, e.g., a recursive procedure’s termination probability (1/2) faster than Kleene iteration, and reports experiments showing NPA-PMA can outperform Kleene iteration with reusable artifacts available.
AI-written summary · about
chapters (12)
- 0:00Newtonian program analysis intro
- 1:26Traditional data flow pipeline
- 3:13Termination probability with semirings
- 5:01Newton's method for equations
- 7:08Newtonian analysis framework
- 12:29Limitations of prior analysis
- 13:33Extending to multiple branches
- 15:57Markov algebras combined
- 16:38Solving equations with Newton
- 17:42Case studies evaluation
- 18:25Key takeaways future work
- 18:45Q&A
related talks
15mStructural Abstraction and Refinement for Probabilistic Programs
01h 05mGraph Algorithms in the MPC Model
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
15mProducts of Recursive Programs for Hypersafety Verification
20mThe Complexity of Infinite-Horizon General-Sum Stochastic Games
29mAmplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers
22mCompositional Programming and Testing of Dynamic Distributed Systems
20mDeciding Asynchronous Hyperproperties for Recursive Programs