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$PMA上的正则无穷树方程系统。NPA-PMA允许分析提供非迭代策略以求解线性化方程。实验评估表明：（i）NPA-PMA在超越Kleene迭代方面具有显著潜力；（ii）该框架为设计程序分析提供了高度的通用性。