标题：Newtonian Program Analysis of Probabilistic Programs

作者：王迪、Thomas Reps

摘要：概率程序由于其量化特性，对设计可组合、高效的程序分析提出了挑战。当前，许多概率程序的分析依赖于迭代近似，而本文提出NPA-PMA，一个过程间数据流分析框架，用于设计和实现对具有非结构化控制流、非确定分支和递归调用的概率程序的程序分析，并且可以部分使用非迭代算法。NPA-PMA基于牛顿程序分析（NPA），其本质是牛顿法在半环上的推广。设计NPA-PMA的关键挑战在于处理多种分支结构，这些结构既出现在分析抽象域的代数结构，有出现在编码程序控制流的方程组中。具体而言，半环支持单一的分支结构，而NPA-PMA涉及三种分支结构（条件、概率以及非确定）。

我们的工作提出ωPMAs来表示不同分析的共同部分，采用正则无限树表达式来编码具有非结构化控制流的概率程序，并提出一种线性化方法，使得牛顿法可以用于求解基于ωPMAs的正则无限树方程组。NPA-PMA在实例化时允许分析实现者提供一种非迭代策略来求解线性化的方程。我们的实验评估表明，NPA-PMA 在概率程序的程序分析上具有相当的潜力超越Kleene迭代法，并且在设计程序分析方面提供了很好的通用性。

标题：Programmable MCMC with Soundly Composed Guide Programs

作者：Long Pham、王迪*、Feras A. Saad、Jan Hoffmann

摘要：概率编程语言（PPL）为灵活表达概率模型和自动求解贝叶斯推断提供了语言支持。具有可编程推断的PPL使用户能够通过使用针对特定模型程序定制的引导程序来定制推断算法，从而获得改进的推断结果。然而，引导程序中的错误可能会损害推断的统计可靠性。本文介绍了一种新的基于协程的框架，用于验证一类广泛使用的MCMC推断算法中用户编写的引导程序的正确性。我们的方法基于一个新型类型系统，该系统描述了模型程序与一系列引导程序之间的通信协议，每个引导程序可以更新模型程序所定义的随机变量的一个子集。我们证明，通过将引导类型转换为具有有限范数的上下文无关过程，可以在多项式时间内检查模型与引导之间的结构类型等价性。这种联系产生了一种高效的类型推断算法，适用于包含递归调用和条件分支等灵活构造的概率程序。我们还提出了一种覆盖检查算法，该算法验证顺序组合的引导程序与模型程序所定义的概率模型定义域一致，这是多引导MCMC推断的关键可靠性条件。实验评估表明，我们的类型推断和覆盖检查算法能高效地推断类型并分析现有静态分析无法处理的可靠引导程序或不可靠引导程序。

标题：Semantics Lifting for Syntactic Sugar

作者：关智超、曹毅远、余泰来、王子恒、王迪*、胡振江

摘要：语法糖在工程编程语言中起着至关重要的作用。它提供了方便的语法和更高层次的抽象，正如它在通用和特定领域环境中的广泛使用所证明的那样。不幸的是，将包含语法糖的程序翻译成宿主语言的传统方法可能会导致抽象泄漏，破坏便利性的承诺，阻碍程序理解。为了应对这一挑战，我们引入了语义提升的概念，旨在静态地推导语法糖的自包含评估规则。更具体地说，我们提出了一种语义提升框架，该框架由以下部分组成：（i）一种通用算法，用于从宿主语言的语义和解糖规则中导出语法糖的宿主无关语义，（ii）提升语义的正确性和抽象性的表述，以及（iii）对确保提升语义可证明正确和抽象的充分条件的系统研究。为了评估我们的语义提升框架，我们实现了一个名为Osazone的系统，并进行了几个案例研究，证明我们的方法对于实现特定领域的语言是灵活、有效和实用的。

标题：Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks

作者：鄢振宇、张昕*、狄鹏（蚂蚁集团）

摘要：基于反例的抽象精化（Counter-example Guided Abstraction Refinement， CEGAR）是程序分析中一种自动选择合适抽象的方法，它能够找到高精度且时间开销低的抽象。过去的工作大多将CEGAR建模为基于SAT/SMT的约束求解问题。由于这些问题复杂度较高，这些CEGAR方法可扩展性较差，往往难以被应用于大型程序或较复杂的分析。

为了解决这一挑战，我们提出了一种结合图神经网络的方法，以提升基于Datalog的程序分析的CEGAR可扩展性。具体而言，我们的方法首先从Datalog求解器的计算中提取出图，然后使用图神经网络基于图结构对图上的抽象参数进行打分。然后，通过忽略分数较低的抽象参数，我们将原本的约束求解问题转化为更小的问题，完成对解空间和约束求解问题的大小的约简。由于我们的方法可以直接从Datalog求解器的计算中提取图而无需针对特定分析的领域知识，我们的方法理论上可以广泛适用于基于Datalog的各种参数化程序分析。我们在一个指针分析和一个类型状态（typestate）分析上验证了我们的方法。相比于基线方法，在大型程序上，我们的方法分别能够求解2.83倍和1.5倍的报告，显示出显著的性能提升并证明了方法的泛用性。

标题：Learning Abstraction Selection for Bayesian Program Analysis

作者：张羿凡、石元峰、张昕*

摘要：在本文中，我们提出了一种基于学习对贝叶斯程序分析进行抽象选取的方法。贝叶斯程序分析通过将概率附加到规则上将程序分析转化为贝叶斯模型，它可以计算分析结果成立的概率，并通过泛化用户反馈、测试结果等后验信息来更新这些概率。贝叶斯程序分析所基于的抽象在很大程度上影响着它泛化这些后验信息的效果。已经有大量的工作研究如何为传统程序分析选取抽象，但这些工作对贝叶斯程序分析并不有效，因为它们的优化目标并不是泛化能力。我们提出了一个从有标签程序中学习的数据驱动框架来解决这一问题。该框架从一个抽象出发，根据分析推导结果决定如何改变该抽象。为了通用，它只考虑分析推导图上的属性；为了有效，它考虑了抽象改变前后分析推导结果的差异。我们在数据竞争分析和线程逃逸分析上展示了我们方法的有效性。