程序设计语言领域顶级会议OOPSLA'25近日公布论文录用名单，程序设计语言研究室四篇论文被该会议录用。

论文1

标题： Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences.

作者： Tianchi Li, Xin Zhang.

摘要： 在贝叶斯程序分析中，一个核心挑战是如何系统地将在形式规范（如类型注解）中发现的形式信息与在代码注释或文档等来源中发现的非形式信息相结合。本文提出了一种通过“软证据”（Soft Evidences）来统一这两种信息的方法。与传统分析中必须严格满足的“硬规则”不同，软证据允许分析以概率方式整合非形式信息。我们将用户引导的程序分析问题表述为求解硬规则和软规则的组合：硬规则捕捉健全性，而软规则捕捉近似程度和用户的偏好。这种方法使得分析能够利用可能不完全准确但信息丰富的非形式提示，从而在不牺牲形式保证的情况下提高分析的精度和实用性。

论文2

标题： Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials.

作者： Qihao Lian, Di Wang.

摘要： 本文介绍了RaRust，一个针对类型良好（well-typed）的Rust程序的、基于类型的线性资源界限分析。RaRust遵循“自动摊销资源分析”（AARA）的方法论来构建一个感知资源的类型系统。为了支持Rust的借用机制，包括共享借用和可变借用，RaRust引入了“共享预言势”（shared prophecy potentials）和“新颖预言势”（novel prophecy potentials）来组合地推理借用。为了证明RaRust的健全性，本文提出了“感知资源的借用演算”（RABC），作为最近提出的“低级借用演算”（LLBC）的一个变体。RaRust原型实现的实验评估表明，RaRust能够为具有共享和可变借用、再借用、堆分配数据结构、循环和递归的Rust程序推断出符号化的线性资源界限。

论文3

标题： Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis.

作者： Guanlin Chen, Ruyi Ji, Shuhao Zhang, Yingfei Xiong.

摘要： 版本空间代数（Version space algebra, VSA）是用于表示程序集合的有效数据结构，并已广泛用于程序综合。尽管取得了成功，但基于VSA的综合在处理大量示例时效率低下是一个关键缺点。然而，两个VSA的交集可能比原始VSA大得多——这种效应在迭代过程中累积，使得中间VSA的规模迅速爆炸。在本文中，我们旨在降低综合中VSA交集的成本。我们研究了迭代交集的过程，并观察到，尽管此过程可能会构建一些巨大的中间VSA，但其最终的VSA在实践中通常很小，因为只有少数程序能通过所有示例。利用这一观察，我们提出了“多路交集”（multi-way intersection）的方法，它直接将多个小的VSA相交为最终结果，从而避免了先前构建巨大中间VSA的瓶颈。此外，由于先前的交集算法对于多个VSA效率低下，我们设计了一种新颖的算法来避免大多数不必要的VSA节点。我们将我们的方法集成到两个SOTA的基于VSA的综合器中，在4个不同的数据集、994个综合任务上进行了评估；结果表明，我们的方法可以显著提高基于VSA的综合性能，最多可多解决105个任务，并带来7.36倍的加速。

论文4

标题： On Abstraction Refinement for Bayesian Program Analysis.

作者： Yuanfeng Shi, Yifan Zhang, Xin Zhang.

摘要： 贝叶斯程序分析是一种系统性的方法，通过将传统程序分析中的逻辑推理转换为贝叶斯推理，从而从外部信息中学习以提高准确性。然而，一个关键的挑战是找到正确的抽象（abstraction），这个抽象必须既足够精确以验证感兴趣的属性，又足够粗糙以确保可扩展性。为了解决这个问题，我们提出了一种受“反例引导的抽象细化”（CEGAR）框架启发的方法，以动态搜索抽象。我们的关键创新是应用条件独立性理论来细化抽象，以便消除不正确的泛化。我们评估了该方法在多个基准程序上的表现，结果表明我们的方法能够自动发现既精确又高效的抽象，其性能显著优于使用固定抽象的现有方法。