• 声明式程序分析中的通用可扩展性（基于选择组合剪枝技术）

  摘要在过去几十年中，用于固定点计算的Datalog引擎为静态程序分析带来了巨大的好处。使用Datalog进行程序分析可以编写出声明性强、易于维护的规范，同时不会牺牲性能，实际上通常比手工编写的算法更快。然而，这些好处也伴随着一定程度的控制权丧失。Datalog的计算是自底向上的，这意味着所有推理（从一组初始事实开始）都会被执行，并且所有推理结果都是计算的输出。实际上，几乎所有用Datalog表示的程序分析在面对某些输入时都会变得不可扩展，因为需要计算所有结果，即使部分答案就已经足够满足需求。在这项工作中，我们提出了一种简单、统一且优雅的解决方案，具有很高的实际效果，几乎可以应用于任何基于Dat

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 高效的分而治之线性化可行性监控方法

  摘要线性化已成为指定并发数据结构实现正确性的事实标准。虽然正式验证这些实现仍然具有挑战性，但“线性化监控”已成为排除自定义实现早期问题的一个有前景的初步步骤，并且是进行压力测试的关键组成部分。在这项工作中，我们对线性化监控问题进行了算法研究，该问题旨在检查从并发数据结构实现中获得的执行历史是否具有线性化特性。尽管普遍认为这个问题在一般情况下是难以解决的，但对其何时可解的系统理解仍然缺失。我们重新审视了这个问题，并首先提出了一个统一的“分而治之”算法框架来设计线性化监控方法。该框架的核心是识别给定历史中的特殊“保持线性化”值——这些值的存在会产生一个等线性化的子历史（通过移除这些值对应的操作获得

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 分而治之：一种基于组合学的博弈论安全方法

  摘要我们提出了一种组合方法，用于结合和扩展在去中心化系统安全（如区块链）静态分析中的自动化推理能力。我们的重点在于对这些系统的博弈论安全分析，这使我们能够研究用户行为背后的经济激励因素。在这种情况下，特别重要的是要证明偏离去中心化协议的预期、诚实行为并不会带来任何利益：只要用户遵循协议，无论其他用户如何行为，他们都不会受到经济损失。对区块链协议的这种经济分析可以编码为一阶实数算术理论中的自动化推理问题，从而将博弈论推理简化为满足性模理论（SMT）问题。然而，将整个博弈论模型（称为“博弈”）作为一个单一的SMT实例进行分析并不足以处理具有数百万交互行为的协议。为了解决这一挑战，我们提出了一种基于

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• Rust中分布式程序的精炼方法论

  摘要精细化（Refinement）是将一个抽象的系统模型转化为一个具体的、可执行的程序，使得为抽象模型定义的属性能够直接应用于具体实现中。这种方法在开发经过验证的大型系统中取得了成功。然而，现有的精细化技术存在一些局限性，这些局限性限制了它们的实际应用价值。自顶向下的精细化技术虽然能够自动生成可执行代码，但生成的实现通常性能不佳；而自底向上的精细化技术虽然可以对现有的高效实现进行推理，但对代码结构、精细化证明的结构以及所使用的验证逻辑和工具有着严格的要求。在本文中，我们提出了一种新的自底向上精细化方法，旨在克服这些局限性。该方法利用了“受保护转换系统”（guarded transition s

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 具有保证精度的浮点数神经网络分类的量化技术

  摘要尽管神经网络取得了巨大的成功，但其计算成本仍然非常高。量化技术可以降低这一成本，但可能会导致原始浮点网络的分类结果发生变化，即使训练过程已经考虑了量化的因素。在这项工作中，我们依靠验证机制来设计修正系统，以便在推理时检测并消除分类不一致的问题。关键思想是用最大分类置信度来过度近似不一致输入的空间。计算这种置信度的主要挑战在于需要分析量化的网络，而这会引入极高的非线性。我们提出了CoMPAQt算法来计算这种置信度。CoMPAQt利用混合整数线性规划（MILP）中对量化的新颖编码方式，并结合定制的线性松弛技术来降低计算复杂性。为了缩小搜索空间，该算法将量化网络与其浮点对应网络的计算结果联系起来

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 盒子里有什么：基于人体工程学的捕捉技术，以及超越通用数据结构的表现力追踪功能

  摘要在Scala中，捕获类型的功能将静态效果和资源跟踪与对象特性统一起来，实现了轻量级的效果多态性，同时减少了符号表示的复杂性。然而，这种表达能力对于追踪嵌套在泛型数据结构中的特性来说仍然不足，从而阻碍了它们被纳入标准集合库——而这正是广泛采用这些特性的关键前提。这一限制源于系统无法在“箱型类型”的概念中对这些特性进行命名。本文提出了System Capless这一新的类型捕获框架，为“reach capabilities”（rcaps）提供了理论基础。rcaps是一种用于命名“箱内内容”的新机制。该框架将“通用能力”的概念细化为一种新的体系，引入了存在量化和全称量化的概念。直观而言，rcap

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• TailTracer：适用于生产环境的持续尾部追踪技术

  摘要尽管进行了大量的内部测试，但错误仍然常常会出现在部署后的软件中。每当生产环境中的软件出现故障时，收集尽可能多的执行信息对于帮助开发者重现、诊断和修复错误是非常重要的。为了平衡跟踪能力、运行时开销以及跟踪规模之间的矛盾，我们提出了一种适用于生产环境的连续尾迹跟踪（continuous tail tracing）方法。这种方法不仅捕获崩溃堆栈，还记录了函数调用的完整序列及其返回情况。为了减轻大量跟踪数据对输入/输出（I/O）、存储和网络传输带来的压力，我们仅保留跟踪数据的最后一部分。为此，我们设计了一种新型的跟踪解码器以实现精确的尾迹解码，并开发了一种基于路径的有效仪器选位算法来降低开销。我们

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 同步行为检查：一种发现编译器优化遗漏的方法

  摘要编译器是有史以来开发的最基础性的软件之一。编译器的关键组成部分是其优化阶段，该阶段能够提升生成代码的效率。鉴于现代编译器的庞大规模和复杂性，开发自动化技术以改进其优化功能已成为一个重要的研究领域。本文重点关注一类特定问题，即“遗漏的优化”——即编译器未能应用本可以提升代码效率的优化措施。为了检测这些遗漏的优化，我们提出了一种名为“同步行为检查”（Synchronized Behavior Checking，简称）的新方法，该方法通过利用多种优化的协同行为来进行交叉验证。SBC的核心思想在于：一种优化的结果可以验证另一种优化所需的条件是否满足。在实现时，我们基于两种关系（共现关系和互补关系）

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 使用CAHPs进行堆快照匹配与排序：一种基于上下文增强的堆路径表示方法，用于前缀树实现精确路径匹配与部分路径匹配

  摘要GraalVM Native Image 越来越被用于优化运行在 Java 虚拟机（JVM）上的应用程序的启动性能，尤其是函数即服务（Function-as-a-Service）和无服务器（Serverless）工作负载。Native Image 采用提前编译（AOT）技术，将 JVM 应用程序编译成二进制文件，该文件包含预初始化堆内存的快照，从而减少初始化时间并提高启动性能。然而，当访问堆快照中的对象时发生的页面错误会限制这种性能提升。相关研究提出了基于性能分析的优化方法，通过根据对象首次被访问的顺序重新排列堆快照中的对象来减少页面错误，这些信息是通过分析同一应用程序的instrumen

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 通过模糊处理和严谨方法革新量子模拟器

  摘要 量子计算平台在硬件执行之前依赖模拟器来建模电路行为，其中的不一致性可能导致代价高昂的错误。虽然现有的形式化验证方法通常针对特定的编译器组件来管理状态爆炸问题，但它们往往无法发现关键错误。与此同时，传统的测试方法缺乏对边界情况和真实执行场景的系统性探索，从而导致误报和漏报。 我们提出了FuzzQ这一新型框架，它通过将形式化方法与结构化测试生成和模糊测试相结合，填补了这一空白。我们的方法采用差分基准测试，并辅以变异测试和不变量检查。FuzzQ的核心是使用基于Alloy的形式化模型来描述QASM 3.0，该模型编码了量子电路的语义，从而实现自动化分析

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 一种考虑数据稀疏性的自主路径规划加速器，采用硬件/软件协同设计及多级数据流优化技术

  在自动驾驶领域，路径规划是一项至关重要的任务，其核心目标是基于输入的感知和定位信息，生成一条平滑、无碰撞且可执行的路径。由于路径规划既要求高实时性又需要大量计算资源，这对资源受限的自动驾驶硬件提出了严峻的挑战。本文提出了一种面向FPGA平台的端到端路径规划加速框架，该框架专注于加速二次规划（QP）求解，因为QP求解是基于优化的路径规划方法的核心，且计算量最大。通过将问题结构化，我们设计了一种具有自适应稀疏特性的硬件友好的交替方向乘子（ADMM）方法，同时采用高度可并行的预条件共轭梯度（PCG）方法来求解相关的线性系统。我们深入分析了QP中矩阵运算的稀疏模式，并设计了定制化的存储方案以及高效的稀

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• PReMM：基于大语言模型的程序修复方法，用于通过分而治之策略处理多种类型的程序错误

  摘要在最近的研究中，大型语言模型（LLMs）被用来提升自动化程序修复技术的能力。虽然现有的基于LLM的程序修复技术在生成高质量补丁方面相比基于启发式方法、约束求解和学习的方法表现更优，但它们主要针对可以通过修改单个错误方法来修复的漏洞，这极大地限制了这些技术在修复需要跨多个方法进行修改的漏洞时的有效性。在这项工作中，我们提出了PReMM技术，该技术能够有效地生成需要修改多个方法的补丁。PReMM基于三个核心组件技术：错误方法聚类技术，根据方法之间的依赖关系将错误方法划分为不同的组，从而实现分而治之的修复策略；故障上下文提取技术，用于收集有关故障上下文的额外信息，以更好地指导故障诊断和正确补丁的

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 通过类型驱动的变异技术对C++编译器进行模糊测试

  摘要C++是一种用于现代软件开发的系统级编程语言，支持多种编程范式，包括面向对象、泛型和函数式编程。这些范式及其相互作用本身具有复杂性，赋予了C++强大的表达能力，但同时也给编译器在正确实现其类型系统方面带来了重大挑战。类型系统涵盖了类型推断、类型检查、子类型化、类型转换、泛型、作用域和绑定等多个方面。然而，在现有研究中，对C++编译器类型系统的系统性测试仍然鲜有探讨。在这项工作中，我们提出了TyMut，这是首个专门用于测试C++类型系统的工具。TyMut是一种基于变异的编译器模糊测试工具，配备了先进的类型驱动变异操作符，这些操作符经过精心设计，能够针对模板泛型、类型转换和继承等复杂的类型相关

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• HAKV：一种基于热度感知的区域管理方法，用于优化基于LSM树的键值存储的性能

  在当今数据爆炸的时代，大规模数据存储系统面临前所未有的挑战。随着数据量的激增，传统存储技术在性能和效率上逐渐暴露出局限性，特别是在处理频繁写入与偶尔更新的键值对（KV pairs）时。为了解决这些问题，研究者们提出了多种优化策略，其中Log-Structured Merge Tree（LSM-tree）因其将随机写入转换为顺序追加操作而被广泛应用，成为许多KV存储系统的核心结构。然而，LSM-tree的多级结构在处理更新频率较低的KV对时，会导致较高的写入放大（Write Amplification, WA）和读取放大（Read Amplification, RA），影响系统的整体性能。为应对

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 通过“生成式平等饱和度”（Generative Equality Saturation）支持的方法，验证SMT重写器（SMT Rewriters）在重写空间探索（Rewrite Space Exploration）中的有效性

  摘要可满足性模理论（SMT）求解器被广泛用于程序分析和其他需要自动化推理的应用领域。作为SMT求解器的关键组成部分，重写系统负责简化并转换公式以优化求解过程。SMT求解器的有效性在很大程度上取决于其重写系统的稳健性，因此对其验证至关重要。尽管SMT求解器测试方面取得了持续进展，但重写系统的验证仍然是一个尚未充分探索的领域。我们的实证分析表明，开发人员在确保重写系统的正确性和可靠性方面投入了大量精力。然而，现有的测试技术并未充分解决这一问题。在本文中，我们介绍了一种名为Aries的新技术，用于验证SMT求解器的重写系统。首先，Aries采用了一种称为“模拟变异”的策略，该策略主动重塑输入公式以引

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• SampDedup：一种用于非易失性内存中高效内联数据去重的技术，通过采样预测实现去重过程

  在当前数据存储技术迅速发展的背景下，数据去重（Data Deduplication）作为一种高效减少冗余存储空间的技术，逐渐成为研究的重点。数据去重通常包括四个主要步骤：分块（Chunking）、指纹生成（Fingerprinting）、指纹查找（Fingerprint Lookup）和数据管理（Data Management）。传统的存储设备如硬盘驱动器（HDD）和固态硬盘（SSD）主要面临的是I/O瓶颈，但随着新型非易失性存储设备（Non-Volatile Memory, NVM）的出现，直接在NVM上应用数据去重技术却遇到了新的挑战。这些问题主要体现在计算瓶颈、指纹索引和元数据设计的重新

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• HybridPersist：一种支持用户友好且高效持久化编程（PM Programming）的编译器技术

  摘要持久内存（Persistent Memory, PM）凭借其数据持久性，在众多领域得到了广泛应用。然而，程序员必须手动在代码中标注与持久内存相关的操作，以确保系统在崩溃时仍能保持数据的一致性，这一过程既费时又容易出错。在本文中，为了减轻开发持久内存应用程序的负担，我们开发了HybridPersist——一种支持用户友好且高效持久内存编程的编译器工具。一方面，HybridPersist能够自动实现崩溃时数据的一致性，对程序员的干预极小，几乎不需要额外添加注释；另一方面，它通过一系列专门的分析步骤提升了持久内存程序的性能和正确性。针对知名基准测试的评估结果表明，HybridPersist在编程

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 调整随机生成器：基于属性的测试作为概率编程的一种方法

  摘要基于属性的测试（Property-Based Testing, PBT）通过使用随机生成的输入来评估软件，从而验证软件是否符合可执行的规范。PBT 用户生成测试输入的标准方法是使用生成器，这些生成器描述了如何通过随机选择来采样测试输入。为了实现测试输入的合理分布，用户必须调整生成器的参数，即确定各个随机选择的权重。不幸的是，很难理解如何选择这些权重以实现所需的分布，因此这一过程非常繁琐，并且限制了实际可以实现的分布范围。在本文中，我们开发了用于生成器自动离线调整的技术。给定一个具有未确定符号权重的生成器和一个目标函数，我们的方法会自动学习这些权重的值，以优化目标函数。我们描述了一些有用的目

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 两种用于静态分析的快速字节码前端实现方法

  摘要在Java的静态分析框架中，字节码前端是一个关键组件，它将复杂的、基于栈的Java字节码转换为更易于分析的、基于寄存器的、带类型的3地址代码表示形式。这种转换通常会显著影响分析框架的整体性能，尤其是在处理大规模Java应用程序时，因此字节码前端的效率对于静态分析至关重要。然而，目前主流的Java静态分析框架Soot和WALA尽管经过了时间考验并被广泛采用，但在效率方面仍存在局限性，这限制了它们提供更好用户体验的能力。为了解决效率问题，我们引入了一种新的字节码前端。通常，字节码前端包括两个关键阶段：（1）将Java字节码转换为无类型的3地址代码；（2）对这种代码进行类型推断。对于3地址代码的

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• HopScotch：一种整体性的方法，用于在NPU上实现数据布局感知的映射，以提升高性能DNN推理的效率

  现代深度神经网络（DNNs）在多个领域得到了广泛应用，其规模迅速扩展，常常包含数百层，每层具有不同的类型和配置。为了加速DNN的执行，专门的硬件解决方案，即神经处理单元（NPUs），已被开发出来。然而，这种DNN模型的层异构性可能会导致在NPUs上的性能下降。例如，虽然某一层的执行或数据流通常与特定的数据访问顺序相关联，但芯片内存中的数据布局可能与之不匹配，从而引入布局重排的空周期。鉴于DNNs中的大量异构层，这种布局重排的开销为实现高效的端到端DNN推理提出了新的挑战。为了解决这一问题，本文介绍了一种全面的数据布局感知映射方法，称为HopScotch，用于将DNN映射到NPUs上。首先，Ho

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

知名企业招聘：