• LLVM AArch64后端的翻译验证

  摘要LLVM的后端将其中间表示（IR）转换为汇编代码或目标代码。除了寄存器分配和指令选择之外，这些后端还包含许多与编译器中间代码阶段相关的组件：数据流分析、公共子表达式消除、循环不变量代码移动以及一种称为“机器IR”（MIR）的一级中间表示。实际上，这种类型的编译器后端本身就是一个高度优化的编译器，它涉及数百万行复杂C++代码所带来的所有正确性风险。为了增强对LLVM后端工作正确性的信心，我们开发了arm-tv工具，该工具可以正式验证LLVM IR与AArch64（64位ARM）代码之间的转换。虽然这不是针对LLVM的首个转换验证项目，但我们在多个方面推动了技术的发展：arm-tv是一个能够强

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 连续张量抽象：索引为实数的情况

  摘要本文介绍了连续张量抽象技术，使得张量索引可以取实数值（例如，A[3.14]）。同时，文中还展示了连续张量代数表达式，如 Cx,y = Ax,y ∗ Bx,y，其中索引定义在连续的域上。这项工作扩展了传统的张量模型，使其能够处理连续张量。我们的实现支持分段常量张量，可以在有限时间内处理无限域。此外，我们还引入了一种新的张量格式以实现高效存储，并提供了一种代码生成技术用于自动生成内核函数。首次将计算几何和计算机图形等领域的问题用张量编程语言进行表达。我们的方法在多种应用中展现出与领先库中手工优化的内核函数相当甚至更优的性能。与在CPU上手工实现的库相比，基于编译器的实现在进行2D半径搜索时平均

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• P³：通过产品程序对补丁进行推理

  摘要软件系统在不断变化，每个补丁都可能引入新的错误和安全漏洞。虽然为程序提供完整的功能规范是一项极其困难的任务，但编写补丁规范来描述补丁版本相对于未补丁版本的行为（例如，“补丁后的版本是对补丁前版本的重构”）通常相对容易。为了对这类规范进行推理，程序分析器需要同时分析补丁前后的软件版本。在本文中，我们提出了P3，这是一个用于通过产品程序自动化推理补丁的框架。尽管之前已经使用过产品程序，尤其是在安全领域，但P3是第一个能够为实际编程语言（即C语言）自动生成产品程序的框架，支持在实际软件中发现的多种复杂补丁，并提供运行时支持，使得灰盒模糊测试和符号执行等技术能够直接在未修改的代码上运行。我们对Co

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 一种轻量级的类型与效果系统，用于验证安全性：通过基于约束的子类型推断来跟踪永久性和临时性的失效情况

  摘要在许多编程范式中，某些程序实体仅在程序的特定范围内有效，例如那些可能在特定作用域结束时被自动释放的资源。一旦超出这些作用域，相应的实体就不再有效——它们会被永久性地标记为无效。有时，即使在资源的有效作用域内，对该资源的使用也可能暂时失效，例如在遍历可变集合时，因为遍历过程中修改集合可能会导致未定义行为。然而，高级通用编程语言很少允许在类型层面反映这些信息。以往解决这一问题的方法大多依赖于限制变量的别名或捕获行为，但这会降低语言的表达能力。在本文中，我们提出了一种更高层次的多态类型-效应系统，可以静态地跟踪敏感值和资源的永久性及临时性失效情况，而无需任何别名或捕获限制。我们使用布尔代数类型（

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 机会主义的并行Lambda演算

  摘要脚本语言被广泛用于执行诸如调用本地库和网络服务等外部操作。在这些脚本中，执行时间往往大部分被等待外部操作所消耗，这使得传统的单一语言优化方法变得无效。为了解决这个问题，我们提出了一种基于核心lambda演算的新的机会主义评估策略，该策略能够自动并行调度独立的外部调用并流式处理其结果。我们证明了我们的方法是收敛的（即最终能够完成所有操作），同时确保了程序员的原始意图得到保留，并且最终能够执行每一个外部调用。我们在一种名为Opal的脚本语言中实现了这一策略。我们通过使用大型语言模型（LLMs）和其他API来演示Opal的灵活性和性能。在五个示例脚本中，我们将Opal与几种最先进的基线算法进行了

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 基于摘要引导搜索的软件模型检测

  摘要在这项工作中，我们描述了一种名为GPS的新软件模型检测算法。GPS将程序的模型检测任务视为对程序状态的定向搜索，这一搜索过程由基于组合原理的静态分析指导。静态分析生成的摘要不仅用于剔除不可行的路径，还用于驱动测试生成，以探索新的、未被覆盖的程序状态。GPS能够找到证明程序安全性的证据，也能找到证明程序不安全的反例（即能够触发错误的输入）。该算法采用了一种新颖的双层搜索策略，使其在检测具有较长、依赖于输入的错误路径的程序中的错误时尤为高效。为了使GPS具备反驳完备性（即如果在给定足够时间的情况下存在错误，GPS能够找到该错误），我们引入了一种仪器化技术，并证明了这种技术可以在不牺牲整体性能的

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• ApkDiffer：一款用于安卓应用程序的精确且可扩展的跨版本差异分析工具

  摘要软件差异分析（也称为代码对齐）是一种用于区分两个给定软件产品中相似和不同代码片段的基本技术。它能够支持多种关键的安全分析工作，例如漏洞定位、软件抄袭检测等。迄今为止，已经提出了许多专门用于二进制文件对齐的差异分析工具。然而，很少有研究致力于跨版本Android应用程序的差异分析，这在很大程度上阻碍了对实际应用的安全评估。总的来说，现有的差异分析方法通常侧重于可扩展性，但在处理现代应用程序的大型代码库时存在严重的对齐错误。为了解决这一难题，我们提出了ApkDiffer，这是一种针对同一开源Android应用程序不同版本进行差异分析的方法级（即函数级）工具。ApkDiffer通过采用两阶段分解

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 高阶程序时间安全性的抽象解释

  摘要本文提出了一种基于抽象解释的新方法，用于验证递归高阶程序的时间安全属性。尽管之前的研究在理论层面取得了进展并实现了一定程度的自动化，但它们的可扩展性有限。我们首先引入了一种新的基于自动机的“抽象效应域”，用于概括上下文敏感的依赖效应，该领域能够抽象程序环境与自动机控制状态之间的关系。我们的分析还包括一种新的转换器，用于将事件前缀抽象为自动计算出的上下文敏感的效应摘要，并将其应用于基于抽象解释的类型-效应系统中。由于该分析依赖于自动机的参数设置，我们进一步将其扩展到更广泛的历史/注册（或“累积器”）自动机类别，从而能够表达一些无上下文依赖的属性，如输入依赖性、事件求和、资源使用情况、成本、事

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 将 ∀∃ 关系型霍尔逻辑（Relational Hoare Logic）编码为标准霍尔逻辑（Standard Hoare Logic）

  摘要验证实际程序的功能正确性可以分解为两部分：（1）细化证明，用于证明该程序实现了更抽象的高级程序；（2）在高级层次上的算法正确性证明。关系Hoare逻辑是一种强大的工具，可用于实现细化证明，但通常需要超出标准Hoare逻辑的进一步形式化处理。特别是在非确定性环境中，需要使用∀∃关系Hoare逻辑。现有的方法将这种逻辑编码为包含“幽灵状态”和“不变量”的Hoare逻辑，但这些扩展显著增加了形式化的复杂性和正确性证明的开销。本文提出了一种通用编码理论，可以将∀∃关系Hoare逻辑简化为标准（一元）Hoare逻辑。具体来说，我们建议重新定义关系Hoare三元组（triples）的有效性，同时保留原

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 用于量化量子网络行为的语言

  摘要量子网络具备仅使用经典信息无法实现的功能。它们连接具有量子特性的节点，其基本的通信单位是“贝尔对”（Bell pair），即一对纠缠的量子比特。由于量子现象的特性，贝尔对非常脆弱，难以在长距离上传输，因此需要通过中继器网络以及专用硬件和软件来确保所需的结果。与量子网络相关的内在挑战，如对共享资源的竞争和高故障概率，要求对量子网络协议进行定量分析。本文提出了PBKAT，这是一种用于规范、验证和优化贝尔对分发量子网络协议的表达性语言。我们的语言配备了用于表达概率性和可能性行为的原语，并具有对协议执行进行建模的语义系统。我们确定了PBKAT语义系统的性质，并利用这些性质对协议行为进行了定量分析。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 混合精度调优中的稳定性成本

  摘要数值代码通常需要在资源有限的硬件上重复执行，这使得它成为优化的理想目标。提高性能（尤其是在运行时间方面）最有效的方法之一是降低计算的精度。然而，低精度可能会导致显著的舍入误差，从而可能影响结果的准确性。混合精度调优通过为程序中的一部分变量和算术运算分配最低可能的精度来平衡这一权衡，同时确保整体误差保持在可接受的范围内。最先进的工具使用可靠的静态分析或动态采样来验证优化程序的准确性。虽然可靠的方法通常被认为更安全但过于保守，而动态方法则更具进取性且可能更有效，但问题仍然存在：这些方法在实践中究竟如何比较？在本文中，我们首次对现有的浮点程序混合精度调优工具进行了全面评估，提供了可靠的静态方法和

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• MIO：在输入/输出问题面前实现的多宇宙调试

  摘要在微控制器上调试非确定性程序一直是一个极具挑战性的任务，尤其是当错误出现在不可预测的、依赖于输入的执行路径中时。最近出现了一种称为“多宇宙调试”（multiverse debugging）的方法，它通过允许程序员探索所有可能的执行路径来简化非确定性程序的调试过程。当前的多宇宙调试器支持程序路径的正向和反向遍历，有些调试器甚至可以跳转到之前访问过的状态，并在这些状态空间内分支到其他执行路径。不幸的是，使用现有的多宇宙调试器调试涉及输入/输出操作的程序时，可能会发现一些无法访问的程序状态，即那些在常规执行过程中不会出现的状态。这会严重阻碍调试过程，因为程序员可能需要花费大量时间来探索和检查这些

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 用于虚拟化内存地址的模态抽象

  摘要虚拟内存管理（VMM）代码是通用操作系统内核中的关键组成部分，但由于硬件接口的复杂性（页面表是通过写入这些内存位置来更新的，而这些地址本身也是虚拟化的），因此对其功能的验证具有挑战性。以往对VMM代码的验证工作要么仅处理单一地址空间，要么依赖于部分可信的汇编代码。在本文中，我们引入了一种模态抽象方法来描述与特定虚拟地址空间相关的断言：[r]P 表示在以 r 为根的虚拟地址空间中 P 成立。这种模态断言允许不同的地址空间相互引用，从而实现对操作多个地址空间的指令序列的完整验证。有效使用这些断言需要结合其他断言，例如关于内存内容的指针断言——这些断言隐含地依赖于它们所使用的地址空间。因此，我们

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 关于全局变量及其初始化的模块化推理

  摘要许多命令式编程语言提供了全局变量，以实现常见的功能，如全局缓存和计数器。全局变量通常由模块初始化器（例如 Java 中的静态初始化器）进行初始化，这些初始化器由运行时系统自动执行。这些初始化器何时以及以何种顺序执行通常是不可静态预测的。例如，在 Java 中，初始化是在类首次被使用时动态触发的；而在 Go 中，其顺序取决于程序中的所有包。因此，从模块化的角度对全局变量及其初始化进行推理是困难的，特别是因为模块初始化器可能会产生任意的副作用，并且可能存在循环依赖关系。因此，现有的模块化验证技术要么不支持全局状态，要么施加了主流语言和程序无法满足的严格限制。在本文中，我们提出了第一种实用的验证

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• AccelerQ：利用机器学习在量子模拟器上加速量子特征值求解器

  摘要我们提出了AccelerQ，这是一个用于自动调整量子本征求解器（QE）实现的框架——这些量子程序实现了特定的QE算法——它利用机器学习和基于搜索的优化方法来进行调整。AccelerQ并不重新设计量子算法或手动修改现有实现的代码，而是将QE实现视为黑盒程序，并通过结合基于搜索的技术和遗传算法（GA）以及机器学习模型来学习优化其超参数，从而提高准确性和效率，有效地探索QE实现的超参数空间并避免陷入局部最小值。我们的方法基于两个核心理念：1）使用来自较小、可经典模拟系统的数据进行训练；2）使用特定于程序的机器学习模型，利用分子系统中的局部物理相互作用在不同尺度上具有普适性的特点，以实现对更大系统

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 为交互式定理证明合成蕴含引理

  摘要交互式定理证明器（ITP）使程序员能够正式验证其软件系统的属性。ITP用户面临的一个挑战是确定完成证明所需的辅助引理，例如那些定义关键归纳不变量的引理。现有的ITP引理合成方法在合成蕴含关系（即形如 P1 ∧ ⋯ ∧ Pn ⇒ Q 的引理）方面支持非常有限，甚至几乎没有支持。在本文中，我们提出了一种用于合成有用蕴含引理的技术及相关工具。我们的方法采用数据驱动的不变量推理来探索当前证明状态的改进方案，这基于对当前目标和假设的样本评估。我们已经在名为dilemma的Rocq策略中实现了这种方法，并证明了其在为《验证函数算法》教科书中的证明以及之前的引理合成基准测试套件生成必要辅助引理方面的有效

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 在反应式系统中验证异步超属性

  摘要超属性（Hyperproperties）是系统属性，它们关联多个执行轨迹，在指定信息流和安全策略时非常常见。像HyperLTL这样的逻辑通过显式量化执行轨迹来表达反应系统中的时间超属性，即那些能够推理无限执行过程中时间行为的超属性。这类逻辑的一个常见副作用是它们会同步比较被量化的轨迹。这限制了这些逻辑表达异步比较多个轨迹的属性的能力，例如Zdancewic和Myers的观察确定性、McLean的非推断性以及Stuttering细化。我们研究了一种异步HyperLTL（A-HLTL）的模型检测问题，这是一种可以表达跨时间步长比较多个轨迹的超属性的时间逻辑。除了对系统轨迹进行量化外，A-HLT

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 具有经过验证的设计的TraceLinking实现

  摘要在形式上可验证的分布式系统设计与其实现之间存在着重要的正确性差距。最近提出的方法通过自动从形式上验证的设计中提取或编译实现来弥合这一差距。然而，这种编译后的实现的实际运行行为可能会与其设计有所不同。例如，编译器可能存在错误；设计可能对部署环境做出了错误的假设；或者实现配置不正确。在本文中，我们开发了TraceLink这一方法，通过跟踪验证来检测此类偏差。TraceLink将捕获执行行为的跟踪信息映射到相应的形式化设计上。与以往的跟踪验证工作不同，我们的方法是完全自动化的。我们将TraceLink应用于PGo编译器，该编译器可以将Modular PlusCal语言转换为TLA+和Go语言。我

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• SafeTree：微服务的表达式树策略

  摘要基于微服务的应用程序由多个称为微服务的独立组件组成，控制服务之间的通信对于确保安全性至关重要。目前，服务间的通信是通过微服务部署工具来配置的。然而，这些工具仅支持有限类别的单跳策略，这些策略可能过于宽松，因为它们忽略了微服务调用中的复杂服务树结构。能够表达服务树结构的策略可以为开发团队和安全团队提供更细粒度的通信模式控制。为此，我们设计了一种表达能力强的策略语言来描述服务树结构，并开发了一种基于可视化下推自动机的动态执行机制来强制执行这些策略。我们的技术是非侵入式的：它不需要对服务实现进行任何修改，也不需要访问微服务代码。为了实现我们的方法，我们在服务网格（一种新兴的网络基础设施层）之上构

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• Flix：一种用于语言集成数据存储的设计

  摘要 我们全面介绍了Flix编程语言中的Datalog功能。我们展示了程序员如何编写作为Datalog程序实现的函数，并演示了如何使用一等Datalog程序值、rho抽象、参数多态性和类型类来构建模块化且可重用的Datalog程序库。我们描述了若干提升Flix中Datalog编程易用性、灵活性和表达能力的特性，包括inject和query程序结构、head和guard表达式、函数谓词、格语义等。 我们通过几个应用实例来说明Flix中的Datalog编程，包括Ullman算法的实现（用于对Datalog程序进行分层处理）、Ford-Fulkerson算

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

知名企业招聘：