Newtonian Program Analysis of Probabilistic Programs

The following summary was generated by AI from the slides.

This talk extends Newtonian Program Analysis to probabilistic programs by replacing the standard semiring with Markov algebras, which support multiple combine operations for probabilistic, demonic, and conditional branching simultaneously. The key technical contribution is lifting Newton’s method — including syntactic linearization and the linear-correction-term iteration — to this richer algebraic structure, enabling superlinear convergence for fixed-point equation systems derived from control-flow hypergraphs. Case studies on termination-probability analysis and expectation-invariant analysis demonstrate that the approach handles loops, unstructured control-flow, and mixed forms of nondeterminism.