Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on iterative approximation. This article presents an interprocedural dataflow-analysis framework, called NPA-PMA, for designing and implementing (partially) non-iterative program analyses of probabilistic programs with unstructured control-flow, nondeterminism, and general recursion. NPA-PMA is based on Newtonian Program Analysis (NPA), a generalization of Newton's method to solve equation systems over semirings. The key challenge for developing NPA-PMA is to handle multiple kinds of confluences in both the algebraic structures that specify analyses and the equation systems that encode control flow: semirings support a single confluence operation, whereas NPA-PMA involves three confluence operations (conditional, probabilistic, and nondeterministic). Our work introduces $\omega$-continuous pre-Markov algebras ($\omega$PMAs) to factor out common parts of different analyses; adopts regular infinite-tree expressions to encode program-execution paths in control-flow hyper-graphs; and presents a linearization method that makes Newton's method applicable to the setting of regular-infinite-tree equations over $\omega$PMAs. NPA-PMA allows analyses to supply a non-iterative strategy to solve linearized equations. Our experimental evaluation demonstrates that (i) NPA-PMA holds considerable promise for outperforming Kleene iteration, and (ii) provides great generality for designing program analyses.

翻译：由于概率程序具有量化特性，在设计组合式且高效的程序分析时面临重大挑战。许多概率程序分析依赖于迭代逼近方法。本文提出了一种称为NPA-PMA的跨过程数据流分析框架，用于设计和实现针对具有非结构化控制流、非确定性和一般递归的概率程序的（部分）非迭代式程序分析。NPA-PMA基于牛顿程序分析（NPA），该方法将牛顿法推广至半环上的方程系统求解。开发NPA-PMA的关键挑战在于需要处理代数结构（定义分析）和非线性方程系统（编码控制流）中的多重汇合类型：半环仅支持单一汇合操作，而NPA-PMA涉及三种汇合操作（条件性、概率性和非确定性）。本文引入$\omega$-连续前马尔可夫代数（$\omega$PMAs）来提取不同分析的公共部分；采用正则无穷树表达式编码控制流超图中的程序执行路径；并提出一种线性化方法，使得牛顿法适用于$\omega$PMAs上的正则无穷树方程系统。NPA-PMA允许分析提供非迭代策略来求解线性化方程。实验评估表明：（i）NPA-PMA在性能上有望超越Kleene迭代方法；（ii）该框架为设计程序分析提供了高度通用性。