PLDI（CCF A）（共 369 篇）
2026108 篇 · 10(PLDI)
合成后向误差界：后向稳定性
提出可组合的后向稳定性定义与范畴 Shel，并实现工具 eggshel 自动合成数值程序的后向误差界。
SAIL：使用大语言模型构建可靠的抽象解释器
提出 SAIL 框架，利用 LLM 自动合成全局可靠的抽象变换器，将任务形式化为约束优化并用不可靠度代价函数指导搜索。
Expecto：从自然语言描述中抽取形式化规约以构建可信赖的 Oracle
Expecto 用神经符号方法从自然语言意图中自顶向下模块化合成 DSL 形式规约，作为可信赖的规约预言机。
通过分阶段优化的可扩展浮点可满足性求解
提出 StageSAT，用三阶段逐步提升精度的数值优化求解浮点可满足性，兼顾可扩展性与可靠性。
概率程序中高效可编程推断的增量计算
将概率程序编译为密度函数并增量计算，加速多种蒙特卡洛推断且分离式证明保证正确性。
可解元组模式及其在程序验证中的应用
提出可从少量正样本高效推断的（合取）可解元组模式，并用于 CHC 求解器验证递归数据结构程序。
面向长时程机器人任务的神经符号分层学习
提出闭环反例引导合成框架，融合LLM规划、SMT验证与可微行为树合成，实现长时程机器人神经符号策略学习。
版本化 E-Graph
提出版本化 E-Graph，同时编码多个等价集合与共享信息，并证明其正确性，显著提升条件等价场景性能。
面向梯度引导、可适应抽象解释的可演化抽象变换器
提出可演化抽象变换器，用参数化可靠输出空间上的梯度搜索替代固定变换器，实现跨数值域、可适应精度—效率权衡的抽象解释。
WebGPU 着色语言中的 Uniformity 分析
首次形式化研究 WebGPU 着色语言的 uniformity 分析，定义 barrier divergence，修正 WGSL 规范并发现 Chromium 实现缺陷。
选择，而非标注：用于程序消歧的多选查询合成
提出基于多选查询的主动学习范式，通过合成 Hoare 三元组选项实现高效的程序消歧。
最优谓词下推合成
提出有状态 fold 计算的最优谓词下推合成框架，自动生成正确且最优的过滤分解。
面向高阶程序的无需支配关系的 SSA
提出以自由变量为基础、用 φ 函数和函数参数直接表达数据依赖的 SSA 新基础，摆脱支配关系并支持高阶程序。
导航 AND–OR 图修改以调试失败的证明搜索
将 AND–OR 图视为证明系统的部分表示，把失败证明搜索的调试转化为修改证明系统，并统一 why-not 策略。
概率符号执行的范畴语义
提出“符号集合”语义域，并给出解释器自动正确性元定理。
带有置信度的抽象解释：用概率量化数据流分析的精度
为抽象解释的数据流分析建立概率化置信度理论框架，量化分析结果的局部完备性精度。
嵌套归纳类型：Lean 与 Rocq 中有依据且可用的嵌套归纳类型
提出嵌套归纳类型的有效性判据，保证可展开为互归纳类型，并自动生成正确的消去原理。
面向 WCET 估计的路径敏感抽象解释
提出路径敏感抽象解释缓存分析，维护关键路径缓存状态，在保持可扩展性下平均提升 WCET 精度 24.83%。
SuperDP：基于超鞅的差分隐私证伪
提出首个全自动、可靠且半完备的 ε-差分隐私证伪方法，并用超鞅同时搜索反例输入与输出函数。
用前向-后向推理与 Prophecy 简化安全性证明
提出增量式安全证明系统，融合前向推理、时间反转的后向推理与 prophecy 步骤，将复杂归纳不变式拆解为更简单的证明步骤。
面向 Verilog 的精密静态分析探索
为 Verilog 构建模块化精密静态分析套件与基础设施，在真实硬件项目中检出多个未知缺陷。
Neptune：面向GPU局部性与并行性的高级ML算子融合
提出张量编译器Neptune，通过打破依赖并构造代数修正表达式，实现归约算子序列的高级融合与高效注意力。
递归定义量子电路的验证
提出递归定义量子电路正确性的证明系统，并证明其可靠性与相对完备性。
TreeCoder：面向 LLM 代码生成的解码与约束的系统化探索与优化
提出 TreeCoder，把解码策略与约束函数作为可优化组件，通过树搜索系统性探索并自动调优 LLM 代码生成。
用于 ω-正则验证的超鞅层级
提出超鞅证书层级验证马尔可夫链几乎必然满足 ω-正则性质，证明 DVSSM 最强并给出 LexPMSM 合成算法与工具。
受限随机生成器的搜索
提出基于演绎程序合成的受限随机生成器合成方法，并在 Lean 中实现 Palamedes。
唯一不动点的超鞅：一种下界验证的统一方法
提出以超鞅见证不动点唯一性的统一框架，用于概率程序多种定量性质的下界验证。
SAQR-QC：面向量子电路的可扩展近似定量推理逻辑
提出 SAQR-QC 逻辑，通过可控精度损失和局部推理，实现对大规模量子电路的可扩展近似定量验证。
Soteria：作为函数式库的高效符号执行——也许你该写自己的符号执行引擎！
提出 OCaml 库 Soteria，支持直接在源语言语义上构建高效、可组合、可靠的符号执行引擎。
SuperCollider：面向 CUDA 的可扩展且有效的数据竞争检测
提出 SuperCollider，一种仅跟踪线程级状态、无内存开销且可扩展的 CUDA 数据竞争检测器。
加权 NetKAT：一种面向定量网络验证的编程语言
提出参数化于半环的加权 NetKAT 语言，并借助加权自动机实现对定量网络性质的自动判定。
通过语义 E-Graph 改进 EDA 中的等式饱和
提出语义 e-graph 与 Nextmap 引擎，以等式饱和跨高层和低层硬件表示优化 EDA，缓解阶段顺序问题。
高阶并发概率程序的上下文精化
提出首个用于证明高阶并发概率程序上下文精化的高阶分离逻辑 Foxtrot，并在 Rocq/Iris 中机器化验证。
面向契约满足证明的演绎系统
提出相对轨迹相等问题与相对互模拟技术，给出可靠完备的演绎证明系统，并在Rocq中形式化用于CPU契约满足证明。
CRIS：混合验证中的想象力
提出 imaginary specifications，将可执行代码与所有权断言自由混合，并构建 CRIS 框架推广 CCR，支持对未验证代码副作用的模块化推理。
Bonsai：将查询编译为剪枝树遍历
用符号区间分析自动推导树元数据剪枝条件，并将复合查询编译融合为单次树遍历。
Cpp2Rust：将 C++ 自动翻译为安全 Rust
首个将 C++ 程序自动翻译为功能等价且内存安全 Rust 代码的系统，以运行时所有权检查换取安全，并用源到源优化降低开销。
因果性与语义分离
在 Rocq 中机器化证明 d-separation 与受非干扰启发的语义定义等价，为实验设计验证提供语义基础。
Pantomime：通过模拟的构造性泄漏证明
提出基于模拟的泄漏证明，以可执行模拟器作为构造性证明对象，并实现工具 Pantomime 验证硬件泄漏描述。
Let It Flow：异步数据流的形式化验证编译框架
首个对异步数据流编译器进行形式化验证的工作，用能力类型系统与 Lean 机器化证明同时保证确定性与流水线优化。
代码-规约-测试-调试-证明：将分离逻辑规约灵活集成到常规工作流
提出一种基于分离逻辑的单一规约语言，可同时支持运行时断言检查、性质测试与机器验证证明，并集成到常规开发流程。
冗余数组计算消除
提出基于哈希的两级方案 RACE，在循环嵌套中层次化检测并消除数组计算冗余。
重启与精化：跨内存预算的可扩展 IFDS 污点分析
提出 ReFine 迭代重启-精化框架，在内存受限下实现可扩展且可靠的 IFDS 污点分析。
快速原子性监控
提出 AtomSanitizer，以 O(nk²) 时间流式检测冲突可串行化，并首次支持低锁并发运行时监控。
混合量子程序的 Hybrid Path-Sums
提出 Hybrid Path-Sums 符号表示与重写/断言系统，实现混合量子程序的自动形式化验证。
Iris-WasmFX：Wasm 栈切换的模块化推理
在 Rocq 中机械化 WasmFX 并证明类型可靠性，提出 Iris 程序逻辑验证使用效应处理器的 Wasm 程序。
EREQ：带量词的正则表达式与增量式量词消去
提出带量词正则表达式 EREQ，以符号导数做增量式量词消去，替代自动机确定化并高效判定 wMSO。
虚拟化续延
通过虚拟化续延所用的栈空间，在词法效应处理器中完整支持多次性续延，并带来并行执行性能收益。
轨迹引导的效应化测试生成器合成
提出欠近似类型与效应系统，用符号轨迹约束引导合成测试生成器，有效探测带效应黑盒系统。
内存安全的降级语义
提出渐进分配器独立性，用信息流非干扰与降级语义刻画分配器相关的内存安全。
Equality Saturation 中的乐观性
提出可在等价饱和过程中进行乐观抽象解释的统一算法，避免不健全性并提升SSA程序分析精度。
超分离逻辑
提出首个支持堆操作程序中任意量词交替超属性模块化推理的程序逻辑 HSL。
编译为循环神经元
将迭代编译为可微循环神经元，使离散算法可直接嵌入神经网络并加速学习。
SparseZETA：设计高性能 SpMV 程序的智能自动调优器
提出基于行为克隆的智能自动调优器 SparseZETA，单遍决策直接生成高性能 SpMV 程序，显著加速并大幅降低设计成本。
面向量子电路优化的等式饱和
提出 Quasar，用双 e-graph 的等式饱和在限定重写步数内生成量子电路的最低代价优化。
鲁棒程序分析的范畴论基础
用范畴论统一刻画程序分析鲁棒性，并给出设计鲁棒分析的通用方法。
GradInf：梯度估计作为概率推断
提出梯度推断，将概率程序梯度估计归约为概率推断，并实现 GradInf 系统自动构造高效估计器。
预合成：借助更细粒度抽象语义扩展程序合成的规模
提出离线预合成阶段，用树自动机与 oracle 支撑细粒度抽象语义下的快速剪枝，显著加速程序合成。
桥接覆盖率与置信度：基于输入无关性的可靠静态误报消除
提出 RICAN，利用输入无关性与定向模糊测试覆盖关键路径，可靠消除静态分析误报。
枚举非法类型程序以测试类型分析器
提出错误枚举方法，通过构造性地注入类型不匹配生成非法类型程序，系统性地发现类型分析器中的可靠性缺陷。
分析字节：反汇编前的静态二进制分析
提出无需预先反汇编的线性时间后向静态二进制分析，基于超集控制流图并避免非法路径污染。
异构动态逻辑：模程序理论的可证性
提出异构动态逻辑 HDL，把不同动态逻辑视为可提升、可组合的动态理论，实现跨语言程序验证并提供机械化可靠性保证。
&inator：正确、精确的 C 到 Rust 接口翻译
提出首个基于约束求解的正确且精确的 C 到 Rust 接口翻译方法，生成满足借用检查的最简 Rust 声明。
模被测库契约的验证
提出综合库方法模块/上下文契约并用测试引擎校验的客户端验证框架，实现工具 Dualis。
VerusBelt：Verus 面向证明的 Rust 类型系统扩展的语义基础
为 Verus 的核心证明类型及 Rust 生命周期、并发与可变借用建立首个语义可靠性证明。
SIMT-Step 执行：面向 GPU 子组行为的灵活操作语义
提出 SIMT-Step 操作语义，以动态基本块精确刻画 GPU 子组同步执行，并在 TLA+ 与多厂商 GPU 上验证。
与你的 self 一同逃逸：面向可达性类型的可靠且表达力强的带规避（avoidance）双向类型检查
提出首个可靠且可判定的可达性类型双向类型检查算法，自动规避类型中不合作用域的名字，并在 Lean 中机器验证。
Hayroll：将 C 宏与条件编译翻译为 Rust 的模块化包装器
Hayroll 以模块化包装器方式让 C-to-Rust 翻译具备预处理器感知能力，恢复条件编译的可配置性与宏抽象，且不修改底层翻译器。
纯数据并行程序中数组性质的验证
提出一种编译器方法，利用预定义数组性质自动验证含非线性索引的数据并行程序。
Kuiper：使用依赖类型与分离逻辑的正确且高效的 GPU 编程
提出嵌入 F* 的依赖类型 GPU 编程语言 Kuiper，扩展分离逻辑以证明内核正确性并编译为高效 CUDA。
一种高效的流式 BPE 分词算法
提出基于合并规则延迟界的流式 BPE 分词算法，以常数内存和线性时间完成分词。
概率高阶分离逻辑中的差分隐私模块化验证
提出概率高阶分离逻辑，将隐私预算作为分离逻辑资源，模块化验证通用语言中的差分隐私实现。
使用类型化视角的模块化 GPU 编程
提出 Prism 语言与 typed perspectives，以类型层面区分线程控制粒度，在保持 GPU 高性能的同时恢复模块化编程。
带分支重排序的函数合并：参数化算法与复杂度
首次从算法与复杂度角度研究允许分支重排序的函数合并，证明其 NP 难，并基于分支因子与嵌套深度给出 FPT 算法及硬度结果。
将数据布局与包围体层次结构解耦
提出 DSL 与编译器 Scion，将 BVH 数据布局与遍历算法解耦，支持体系结构无关的布局优化空间探索。
NEURA：面向粗粒度可重构架构的统一可重定向编译框架
提出统一可重定向的CGRA编译框架NEURA，用谓词类型系统纯数据流IR解决控制流与数据流不匹配。
通过可撤销能力（Capabilities）实现 Typestate
将流不敏感的 capability 机制扩展为流敏感，解耦能力生命周期与词法作用域，实现安全且表达力强的 typestate 编程。
基于寄存器集合自动机的带反向引用正则表达式高效匹配
提出寄存器集合自动机（RSA），将一类带反向引用的正则表达式确定化，实现线性/二次时间匹配并提升鲁棒性。
内在正确的算法与递归余代数
提出 well-founded functor 框架，使余代数的类型自动保证递归性，从而内在获得算法正确性与终止性。
带有静态重载的句法隐式参数
提出句法隐式参数与静态重载两个正交机制，以简单实现覆盖隐式参数的常见用法。
可互换存储器：面向自动化技术映射与重定向
提出 HDL 级可互换存储器抽象与 Memo 编译器，实现存储器一次编写、自动映射到仿真/ASIC/FPGA 并支持重定向。
CoTenN：使用张量网络的约束优化
提出 QCOP 抽象、约束语言 Masq 与编译器 CoTenN，将带硬约束的量子优化问题自动编译为张量网络并求基态。
Cerisier：能力机器中面向 Attestation 的程序逻辑
首个面向可信、不可信与已认证代码的模块化程序逻辑，支持能力机器中 enclave 证明的端到端验证。
SureDistrib：验证组合异步拜占庭协议的几乎必然终止
提出 SureDistrib 形式化框架，支持概率安全/活性规范与精化组合，并首次机器化证明异步拜占庭二元共识几乎必然终止。
迈向移除 LLVM IR 中的 undef 值
提出 raw memory 类型与 freezing load 扩展 LLVM IR，替代 undef 的最后用途，为彻底移除 undef 铺路。
基于流分析的闭包优化
提出基于高阶流分析的安全空间闭包转换器，优化变量元组共享与寄存器展开，提升 SML/NJ 生成代码性能。
ML 中向后兼容的基于 row 的异常追踪
提出基于 row 多态与子类型的异常追踪类型系统，保持 ML 向后兼容，并在 Rocq 中用关系分离逻辑机械化验证。
相对于网络架构的全局分布式协议可实现性
首次系统研究全局分布式协议相对于网络架构的可实现性，提出网络参数化 Coherence Conditions，并归约到消息缓冲区操作公理，给出复杂度、算法与工具。
经过验证的 OCaml 5 并行调度器
在 Iris/Zoo 中实现并验证 OCaml 5 并行调度器，验证 Chase-Lev 工作窃取队列，提出 Iris 预言变量新抽象。
Pure Borrow：线性 Haskell 遇上 Rust 风格借用
提出 Pure Borrow，在 Linear Haskell 中以纯函数方式实现 Rust 式借用，支持仿射可变引用的并行突变且保持纯度。
用于优化稀疏张量程序的已验证数据结构的机器化代数
提出机器化验证框架，用层级抽象定义和组合稀疏张量格式，并在 ATL 调度重写中可靠地将稠密程序优化为稀疏程序。
将 Strassen 类矩阵乘法算法编译为快速 CUDA 内核
提出 SubCuber，一个面向 Strassen 类矩阵乘法的领域特定编译器，生成高效 CUDA 内核。
语义具体化：随机程序生成的新范式
提出以 CFG 与执行路径为核心的随机程序生成范式，可生成语义正确、可终止且支持任意控制流的程序，用于编译器测试。
固定参数可处理的线性一致性监测
证明以进程数为参数时，栈、队列、优先队列和映射的线性一致性监测是固定参数可处理的。
组合异构一致性的形式化验证基础
首次在 Lean 中机器验证同步传播原则，证明其可为一大类异构一致性协议保证复合内存一致性模型。
面向基于 DPOR 的模型检测器的状态空间估计
提出首个可证明多项式时间无偏估计 Mazurkiewicz 迹数量的 Monte Carlo 方法，用于 DPOR 模型检测的状态空间与开销估计。
具有动态与一等优先级的响应式并行
用细化类型跟踪优先级集合，使响应式并行语言支持动态且一等的线程优先级，并给出吞吐与响应性界。
MatchBox：数据平面可移植性的语义基础
提出 MatchBox，以 Match Algebra 与 GFD 类型系统实现异构匹配-动作表的可移植翻译。
Cobble：为量子计算线性代数编译块编码
提出 Cobble 语言，用高层记法表达矩阵的块编码并自动编译为正确的量子线路，配合成本分析与优化，在多个基准上取得 2.6x–25.4x 加速。
上下文嵌入：通过实例解析实现绑定变量
提出上下文嵌入技术，用实例解析在易用高阶接口与一阶表示间建立类型安全的上下文导向同构。
具有值语义的持久迭代器
提出持久迭代器抽象，将命令式迭代器风格与持久化数据结构的值语义结合，兼顾安全性与迭代器表达力。
FlexHeap：面向托管应用的动态 I/O 感知堆大小调整
提出 FlexHeap，在 JVM 堆与 I/O 页缓存间动态划分 DRAM 预算，权衡 GC 与 I/O 停顿以提升搜索分析应用性能。
多重集上融合关系运算的编译器
提出基于抽象循环IR的关系代数编译器，可在集合与多重集上融合算子并生成高效C++代码。
重新审视部分追踪：非托管语言中安全、高效且并发的垃圾回收
提出并发部分追踪 GC 库，用阶段共识与 hazard pointer 实现非托管语言安全、高效、易集成的并发回收。
通过空间细化绘制程序值图
提出声明式 DSL Spytial，以空间语义和约束求解将程序值渲染为可交互二维图，并支持多语言嵌入与反事实调试。
Python 中的动态检查深度不可变性
为 Python 设计并实现动态检查的深度不可变性，通过 detachment 与 freezability 实现子解释器间零拷贝共享对象。
勘误：Falcon：一种可扩展的分析式缓存模型
对 PLDI 2024 论文 Falcon 的实验评估进行勘误，并给出更新数据。
编辑寄语
介绍 PACMPL 期刊的定位、与 SIGPLAN 的合作及开放获取承诺。
202589 篇 · 9(PLDI)
Bean：一种用于后向误差分析的语言
提出 Bean 语言及带分级 coeffect 与严格线性的类型系统，静态推导浮点程序后向误差界，并用范畴语义证明可靠性。
使用语言模型的类型约束代码生成
提出类型约束解码：用前缀自动机与可居留类型搜索保证 LLM 生成代码良类型，编译错误减少过半。
使用连续优化求解浮点约束
提出基于数学优化的 SMT 浮点约束求解器 Grater，求解数量媲美最强求解器且速度快一个数量级以上。
DR.FIX：在工业规模下自动修复数据竞争
提出 Dr.Fix，结合 LLM 与程序分析在 Go 中自动修复数据竞争，并在 Uber 大规模部署验证。
基于编译器引导大语言模型归约分析的输入中心代码优化
结合编译器与LLM的归约分析自动识别关键输入特征，将输入识别时间缩短44至450倍，支撑输入中心优化。
使用大语言模型对整个项目进行可扩展、经校验的代码翻译
提出模块化、特征映射与类型兼容性检查的 LLM 代码翻译方法，可将万行级 Go 项目可靠翻译为 Rust。
MLIR 的一等验证方言
将形式语义作为一等公民引入 MLIR，设计验证方言以支持编译器 IR 的语义编码与通用验证工具。
引导式张量提升
提出结合枚举合成与大语言模型的程序提升方法，自动学习概率文法启发式，将遗留代码提升到机器学习 DSL。
Roulette：一种表达力强、精确且高效的离散概率编程语言
提出 Roulette，首个兼具高性能精确推断与通用语言特性的离散概率编程语言。
无需担忧应用舍入模式的正确舍入数学库
提出舍入不变输出与舍入不变输入界两种方法，使 RLibm 数学库无需频繁切换舍入模式，性能提升超过 2 倍。
支撑三角形机器（Support Triangle Machine）
提出凸近似提升问题及支撑三角形机器，将单神经元近似提升为更精确的多神经元近似，用于DNN验证。
具有形式化保证的随机变量生成
提出从有限精度 CDF 数值程序自动合成精确随机变量生成器的方法，兼具形式化保证与熵最优性。
Tree Borrows（树状借用）
用树结构替代栈定义 Rust 别名模型 Tree Borrows，更精确刻画 unsafe 代码行为，大幅减少误报并保留与新增编译器优化。
差分隐私的已验证基础
在 Lean 中机械化差分隐私基础，并提供经形式验证的 Laplace 与高斯采样实现。
符号 NetKAT 自动机的主动学习
提出主动学习未知网络 NetKAT 模型（含符号自动机）的算法，并证明其健全性。
使 Iris 失稳
通过引入不稳定资源并调整帧规则，使 Iris 支持堆依赖表达式断言并连接 SMT 求解器。
清除有毒垃圾：在混合流敏感静态分析中恢复精度
通过按来源区分贡献的 narrowing、保守 widening 与抽象垃圾回收，消除全局流不敏感分析中的多余贡献以恢复整体精度。
基于带标签并查集的关系抽象
提出带标签并查集，并基于它构造可高效表示关系约束的抽象域，用于程序分析与 SMT 求解。
面向离散概率程序推断的随机惰性知识编译
提出随机惰性知识编译，使离散概率程序的精确推断可惰性加速，并用序列蒙特卡洛实现近似推断。
导航式编程（Programming by Navigation）
提出导航式编程合成问题，保证规约细化中所有且仅有有效下一步，并高效求解。
放宽别名分析：探索尚未探索的空间
反向研究别名分析：系统性移除（而非精化）别名信息，发现其在 LLVM 中影响甚微，仅少数查询真正关键。
验证语义引导综合（SemGuS）问题的解
将 SemGuS 解验证归约到 μCLP 有效性，并扩展 SemGuS 以支持非确定性与反应式综合。
面向数据库支撑应用的指针分析
提出首个面向 Java 数据库支撑应用的指针分析 DBridge，统一建模应用代码、数据库框架与 SQL，并配套微基准 DB-Micro。
Graphiti：桥接图数据库与关系数据库查询
提出将 Cypher 图查询与 SQL 关系查询的等价性检查归约为 SQL 查询等价性验证的方法与工具 Graphiti。
面向持续翻译验证的优化导向编译器模糊测试
提出 Optimuzz，将优化导向灰盒模糊测试与翻译验证结合，持续检测编译器错误优化，在 LLVM 与 TurboFan 上优于现有工具并发现 55 个新误编译 bug。
实用类型推断中的层级（Levels）
首次系统形式化类型推断实现中广泛使用的 levels 技术，并说明其可用于实际类型推断实现。
面向 Node.js 包的自动化漏洞利用生成
首个能合成含复杂调用序列的可用漏洞利用的工具 Explode.js，用于确认 Node.js 包中的真实漏洞。
MarQSim：在量子模拟的编译器优化中协调确定性与随机性
提出 MarQSim 编译框架，用马尔可夫链与最小费用流统一量子哈密顿模拟编译中的确定性与随机性优化。
Morello-Cerise：Arm Morello 能力硬件架构的强封装性证明
在 Morello ISA 全规模模型上机器化证明任意不可信代码存在时软件组件的强安全封装性质。
MISAAL：基于合成的自动生成高效且可重定向的语义驱动优化
Misaal 用硬件指令形式语义离线剪枝重写规则、在线轻量项重写，实现快速可重定向的合成优化编译器。
Nola：用于在 Iris 中验证终止性的无 later 模态幽灵状态
提出 Nola 框架实现无 later 模态的高阶幽灵状态，支撑 Iris 中对 Rust 程序终止性等完全正确性的验证。
图形着色器编译器后端的发散感知测试
提出 ShaDiv，针对图形着色器编译器后端，利用 GPU 线程控制流与数据流发散模式生成测试，发现 12 个后端缺陷。
认证编译器 à la carte
为 Rocq 引入晚绑定、mixin 组合与族多态的扩展机制（Rocqet 插件），使 CompCert 级别的认证编译器可模块化、可复用、按需组合。
Slotted E-Graph：为（绑定）变量提供一等支持
提出槽位 E-Graph，将绑定变量作为内建一等特性，使仅变量名不同的项共享表示，避免 E-Graph 膨胀。
通过控制流一致性分析增强 LLVM 调试信息更新的健壮性
提出首个自动识别并修复 LLVM 优化中调试位置更新错误的技术，并落地为 MetaLoc。
在松弛内存分离逻辑中验证无锁遍历
首次在松弛内存一致性下形式验证无锁链表、跳表及跳表优先队列，提出逐键线性化历史规约与 shadowed-by 关系。
面向非确定性程序与编译器的平滑、集成式密码学常量时间证明
首次用omnisemantics形式化非确定性程序的常量时间规范，并在Coq中端到端验证密码编译。
概率精化会话类型
提出概率精化会话类型 PReST，以符号化精化推理支持非常量概率的并发概率程序验证。
面向自动化程序翻译的程序骨架
提出程序骨架方法，将跨语言翻译分解为可机械翻译的骨架与可综合的代码片段，实现 Python 到 JavaScript 翻译。
Thrust：面向 Rust 的基于预言的精化类型系统
提出基于预言的 Rust 依赖精化类型系统与推断工具 Thrust，实现自动化的函数正确性验证。
语义正则表达式的成员测试
研究语义正则表达式（SemREs）的成员测试问题，即判定字符串是否匹配带外部 oracle 查询的正则模式。
精确循环界分析
提出通过前置条件合成计算程序精确循环界的方法，并实现工具 ELBA 验证其有效性。
量子纠错程序的高效形式验证
提出量子纠错程序的形式验证框架，含证明系统、VC 求解与 Coq 形式化，并实现 Veri-QEC。
半自动化 Rust 验证的混合方法
提出将 Rust 验证分为自动验证安全代码与半自动验证 unsafe 代码的混合方法，并实现 Gillian-Rust 与 Creusot 联动。
PulseCore：面向依赖类型程序的非直谓并发分离逻辑
提出 PulseCore，一个面向依赖类型高阶并发程序内在证明的并发分离逻辑，并在 F* 中机械化验证。
现代 GPU 上的任务式张量计算
提出任务式张量编程模型 Cypress 及其编译器，以顺序语义屏蔽异步数据搬运与同步，性能比肩专家手写 CUDA。
AWDIT：一种最优的弱数据库隔离测试器
提出 AWDIT，可证明最优地测试 RC、RA 和 CC 弱隔离级别，并显著提升效率。
Ripple：面向空间数据流架构的异步编程
提出语言与架构 Ripple，用异步迭代器、共享内存原子操作与任务并行接口消除抽象倒置，支持非规则计算。
字符串变换合成的并发方法
提出首个并发字符串变换合成算法，通过异步协调演绎与枚举过程，并实现工具 Synthphonia 显著提升性能。
QVM：量子门虚拟化机器
提出可扩展的量子门虚拟化系统，通过虚拟电路IR、编译器与运行时在小型含噪QPU上高保真执行大规模量子电路。
液体类型（Liquid Types）的可用性障碍
通过研究揭示 LiquidHaskell 开发者面临的九类可用性障碍，为液体类型系统设计提供依据。
高效的可线性化监控
为并发栈、队列、集合与多重集给出更快的线性一致性监控算法，纠正既有错误证明，并实现工具 LiMo。
LiDO-DAG：验证基于 DAG 的共识协议安全性与活性的框架
提出 LiDO-DAG 并发对象模型，并在 Coq 中为三种 DAG 共识协议机化验证安全性与活性。
利用 C/C++ 程序中的未定义行为进行优化：性能影响研究
首个大规模实证研究表明，在 C/C++ 中利用未定义行为进行优化带来的端到端性能提升甚微。
RefinedProsa：将响应时间分析与 C 验证连接起来用于无中断调度器
在 Rocq 中连接 RefinedC 的 C 验证与 Prosa 的响应时间分析，首次机器验证无中断 C 调度器的时序保证。
Web 与流导向的保良类型性程序变换
提出以 web（生产者-消费者集合）为变换单位的中间语言与流导向变换，并用基于合一的类型分析保证变换保持良类型性。
面向并发安全的动态区域所有权
提出动态区域所有权模型，为动态类型语言提供可解释的并发安全所有权检查。
前缀下的主类型推断：重新审视静态重载
提出 HMQ，将 HM 类型规则重构为“前缀下的类型推断”，直接推出与 Algorithm W 一致的主类型，并简化 FreezeML、HMF 及 Koka 静态重载的形式化。
利用不可变性为乐观遍历验证 Hazard Pointer
提出利用标记节点不可变性的 Hazard Pointer 验证策略，支持乐观遍历的无锁结构，并在 Rocq/Iris 中证明其安全性。
RRR-SMR：减少、重用、回收——实用无锁数据结构的更好方法
提出 RRR 通用方法，使 SMR 下的无锁数据结构能安全重用与移动节点而无需重新分配，并给出 Michael-Scott 队列的高效特化实现。
基于补丁—协调对应关系的快速直接操纵编程
为长时程序引入与补丁对应的协调过程，直接更新输出而跳过前向求值，从而降低交互延迟。
Iso：请求私有的垃圾回收
提出 Iso——首个面向 Java 的请求私有垃圾回收器，用 mark-region 堆与机会式复制显著降低请求型服务的 GC 开销。
在松弛内存分离逻辑中验证通用 RCU 的内存回收
首次在松弛内存模型下形式化验证具备模块化规约、可切换临界区与并发写者支持的通用 RCU。
CRGC：Pekko 中容错的 Actor 垃圾回收
提出首个容错且可回收循环垃圾的 actor 垃圾收集器 CRGC，并在 Pekko 中实现与评估。
使并发硬件验证顺序化
提出受 Bluespec 启发的形式语言 Fjfj，通过语言限制将并发硬件模块验证顺序化，并在 Coq 中证明 refinement 定理。
并行流式计算的函数式语义
提出核心语言 λ∨，用流序统一函数式编程与确定性分布式计算的基础。
面向 Rust trait 错误的交互式调试器
Argus 将 Rust trait 推断失败的搜索树交互式可视化，按不同调试目标提供多视图，显著提升错误定位效率。
面向基于采样的数据竞争检测的高效时间戳
提出新 freshness 时间戳、专用数据结构与算法，降低采样式 HB 数据竞争检测的时间戳开销，并证明其实例最优。
多阶段关系编程
将多阶段编程引入关系式编程，扩展 miniKanren 以分阶段解释含洞程序，并在综合任务中显著加速。
用 SPARE 优化基于辅助量子比特的量子电路
提出 SPARE，通过重写 compute-uncompute 门序列并利用 ancilla 状态来优化量子电路，且证明重写正确性。
奇点积分与微分的语义
首次为支持奇点积分求值与微分的可微编程语言 SingularFlow 建立指称语义，并证明 Monte Carlo 操作语义是良态估计器。
CompCertOC：支持共享栈的多线程程序的经过验证的组合式编译
提出线程化 Kripke 内存关系与前向模拟，实现共享栈多线程程序的组合式编译验证，构建 CompCertOC。
带天使非确定性的概率 Kleene 代数
引入带天使非确定性的概率 Kleene 代数与自动机，以多重集分布语义克服单子分配律障碍，并证明 Kleene 定理。
StacKAT：无限状态网络验证
提出带栈的网络验证语言 StacKAT，并给出基于有限自动机的等价判定与完备公理化。
基于部分轨迹的程序合成
提出首个从仅记录副作用调用的部分轨迹中，合成含副作用函数、纯函数与控制流程序的方法。
面向弱内存的动态鲁棒性验证
首次提出面向弱内存模型的动态鲁棒性验证，用位置时钟在 C11 下高效检测程序是否仅表现强一致行为。
Polygon：使用冲突驱动欠近似搜索的 SQL 符号推理
提出 Polygon，用冲突驱动欠近似搜索为 SQL 查询生成满足 SMT 属性的输入，以反驳等价性或消歧查询。
鲁棒常数时间密码学
提出 RoboCop：用参数化攻击者模型定义鲁棒常数时间性质，并按应用上下文编译生成定制密码库防护。
依赖 Lambek 演算中解析器与形式文法理论的内在验证
提出依赖 Lambek 演算，用线性类型内在验证解析器只产生合法语法树，并编码正则/上下文无关文法与自动机。
字符串求解中位置约束的统一处理框架
提出基于自动机 Parikh 像归约的位置字符串约束判定过程，避免词方程编码并提升求解效率。
轻量级且局部性感知的黑盒子程序组合
提出 Fern，通过轻量级声明暴露数据依赖模式，在保持模块性的同时融合黑盒子程序，最高加速 5 倍。
高效、可移植且支持参与者数量多态（census polymorphism）的编排式编程
提出 conclave、多位置值与 census 多态，使库级编排编程的分支无需冗余通信且可跨宿主语言移植。
量子寄存器机：量子递归程序的高效实现
提出量子寄存器机及实现技术，以高效执行量子控制流与递归过程调用交织的量子递归程序。
处理选择单子（Selection Monad）
提出带选择续延的代数效应处理器，使程序员能实现感知损失的选择操作，并给出λC语言的操作/指称语义与Haskell实现。
面向 CPU 上 SpMV 的 UZP 稀疏格式的模块化构建与优化
提出基于整数多面体并集的 UZP 稀疏格式，统一 CSR/COO 等格式并支持模块化调优 SpMV 性能。
C++ 程序中动态类型转换的链接时优化
提出 LLVM 链接时优化，用短指令序列替换 C++ 向下转型库调用，并通过修改 vtable 消除冗余 RTTI 数据。
部分求值与全程序编译
提出部分求值变换，将现有解释器无需剖面地AOT特化为动态语言编译器，并在真实引擎上取得显著加速。
用于布局失效的 Spineless Traversal
提出 Spineless Traversal，一种缓存友好的增量布局算法，避免访问辅助节点，显著降低布局延迟。
使用算术表查找的电路优化
提出 FHE 编译器 COATL，利用可编程自举与算术查找表优化布尔电路，使生成电路最高快 1.5 倍。
202489 篇 · 8(PLDI)
Numerical Fuzz：一种面向舍入误差分析的类型系统
提出带线性灵敏度与分级单子的类型系统 Λ_num，静态推导浮点舍入误差的定量界并证明其语义可靠性。
浮点 TVPI 抽象域
提出 TVPI-FP 浮点抽象域，用区间算术重设计算子，高效分析含分支、循环与初等函数的浮点程序。
通过多项式求解的贝叶斯概率程序静态后验推断
提出用多项式求解静态推断贝叶斯概率程序的归一化后验分布边界，并支持 score 递归程序。
结合静态分析与贝叶斯推断的鲁棒资源界
提出 Hybrid AARA，将类型化静态资源分析与贝叶斯推断融合，得到统计可靠且更鲁棒的最坏情况资源界。
Bit Blasting 概率程序
提出 bit blasting 离散化，将混合概率程序转为布尔随机变量上的离散推断，并实现 HyBit。
基于信息流的概率程序编译与变量消除
提出一种编译方法，利用信息流类型系统分解概率计算，将递归概率程序的全局边缘推断化为可处理子问题。
不可行低维线性规划的最大共识浮点解：以凸包为中间表示
提出以凸包为中间表示求解不可行低维线性规划，生成满足最多约束的浮点解，加速正确舍入数学库多项式生成。
面向自适应数据分析的程序分析
将自适应性形式化为程序量化性质，并用加权依赖图分析近似其上界，以辅助选择泛化误差控制技术。
Falcon：一种融合式的路径敏感稀疏数据依赖分析方法
提出 Falcon，将路径敏感内存模型下的析取推理分解为半路径敏感摘要与按需解析，实现可扩展的上下文敏感数据依赖分析。
深度神经网络的输入关系验证
提出差分跟踪与 DiffPoly 抽象域，实现高精度可扩展的 DNN 输入关系验证器 RaVeN。
支持可编程变分推断的概率编程
提出以组合式程序变换支持可编程变分推断，将变分目标写成程序并自动变换为无偏梯度估计器。
用饱和度扩展基于类型的指向分析
提出饱和度机制，使基于类型的上下文不敏感指向分析在保持大部分精度的同时达到 RTA 的可扩展性。
面向 JavaScript 的高效静态漏洞分析：多版本依赖图
提出多版本依赖图 MDG 与 Graph.js 扫描器，在 npm 包漏洞检测中同时降低漏报与分析耗时。
Diffy：数据驱动的配置缺陷发现
提出首个一键式结构化配置分析器 Diffy，通过模板学习与无监督异常检测自动发现配置缺陷。
基于偏斜制表的上下文无关语言可达性
提出偏斜制表策略，通过消除递归非终结符产生的冗余摘要边，加速上下文无关语言可达性求解。
概率程序的等价性与相似性反驳
提出首个全自动、可处理无限状态、带形式保证的概率程序等价性与相似性反驳方法
用抽象解释进行编译
将抽象解释器转化为编译器，把编译 pass 对应为函子域，并用 SSA 抽象域提升分析精度。
面向漏洞评估的定量鲁棒性
提出定量鲁棒可达性与定量鲁棒符号执行（QRSE），自动度量触发漏洞的难度。
函数式张量语言的已验证编译器
为函数式张量语言 ATL 的降级算法提供形式化正确性证明，并用新类型系统修复截断 reshape 的可靠性缺陷。
SMT 理论套利：使用有界理论近似无界约束
提出理论套利，将无界 SMT 约束转为有界约束以大幅加速求解。
RefinedRust：面向 Rust 程序高保障验证的类型系统
提出在 Coq 中证明可靠的精化类型系统，支持 safe 与 unsafe Rust 代码的基础性半自动功能正确性验证。
面向简洁高效全同态加密的自动数据打包张量编译器
提出 Fhelipe 张量编译器，用自动数据打包为全同态加密程序选择并优化张量布局，兼顾易用与性能。
不要写，而是返回：在 C 到 Rust 翻译中用代数数据类型替换输出参数
提出基于抽象解释的静态分析技术，在 C 到 Rust 翻译中识别并消除输出参数，改用元组与 Option/Result 等代数数据类型返回。
超 Hoare 逻辑：（反）证明程序超性质
提出超 Hoare 逻辑，将断言提升到状态集合，可在同一逻辑中证明和反证程序超性质。
用 SpecTec 为 WebAssembly 标准提速
提出 SpecTec DSL 与工具链，将 Wasm 形式规范作为单一事实来源，自动生成规范文档与元级解释器并发现规范错误。
从 Coq 到 OCaml 的已验证提取
在 Coq 中实现并验证从 Coq 到 OCaml 的提取流水线，给出正确性定理与安全互操作保证。
精细输入，退化输出：编译器行为的反直觉世界
揭示编译器在获得更精确信息（死代码、值域）后反而生成更差代码，并自动化测试发现此类问题。
JavaScript 正则表达式的线性匹配
界定了 JavaScript 正则中可线性时间匹配的更大子集，并给出首个非回溯的线性 lookaround 匹配算法。
面向高效缺陷发现的兼容分支覆盖驱动符号执行
提出兼容分支覆盖驱动的符号执行，利用程序依赖分析剪枝冗余路径，加速缺陷发现。
结构化数据的机械化 Hypersafety 证明
提出 LGTM：参数化 Hypersafety 关系分离逻辑，并在 Coq 中机械化验证结构化数据操作。
LiDO：具有基于精化的活性证明的可线性化拜占庭分布式对象
LiDO 模型引入 pacemaker 状态，将 SMR 活性归约为安全性质，并在 Coq 中机器化验证 Jolteon（含流水线）的安全与活性。
SuperStack：通过贪心、约束与 SAT 技术对栈字节码进行超优化
提出 SuperStack，用贪心、MaxSAT 与领域约束加速栈字节码超优化，找到更优等价指令序列。
Falcon：一个可扩展的解析式缓存模型
提出首个可扩展的解析式缓存模型，通过分块计算避免 Presburger 求解器最坏复杂度，将大型仿射程序分析从数小时降至秒级。
以近似解释减少静态分析的不健全性
提出近似解释动态分析，自动推断 JavaScript 动态属性访问的确定事实，用于静态分析减少不健全性并改进调用图构建。
奖励引导的带控制结构的智能体合成
提出奖励引导的程序合成范式 ReGuS，用带循环、条件与过程调用的分层合成算法高效求解长时程机器人控制任务。
密码学服务器的基础性集成验证
在 Coq 中整合多种验证技术，端到端证明裸机密码学服务器的全系统功能正确性与内存上界。
GenSQL：一个用于查询数据库表生成模型的概率编程系统
在 SQL 上增加少量概率查询原语，构建可查询表格数据生成模型的概率编程系统 GenSQL，并给出类型系统、指称语义与可靠性证明。
一个 HAT 技巧：使用符号有限自动机自动验证表示不变式
提出 Hoare 自动机类型，将符号有限自动机融入精化类型，以自动验证依赖有状态库的数据结构表示不变式。
检查正则表达式消歧鲁棒性的静态分析
提出正则表达式消歧鲁棒性概念，证明判定问题为 PSPACE 完全，并给出实用静态分析算法与优化。
量子比特回收再审视
提出量子比特依赖图，将量子比特回收归约为矩阵三角化，给出 NP 难性、启发式求解器与 Coq 验证实现。
用行为契约强化智能合约
提出 Solidity 语言扩展 ConSol，支持将行为契约附加到一等地址并在调用时监控违约，实现模块化的智能合约规约与验证。
基本代数律的自动验证
提出 Propel，自动验证应用代码中的结合律、交换律、幂等律等基本代数律，支持辅助性质猜想与等式/不等式推理。
PL4XGL：一种可解释图学习的编程语言方法
提出图描述语言 GDL 和基于程序合成的可解释图学习模型 PL4XGL，用 GDL 程序解释分类结果。
IsoPredict：用于检测弱隔离数据存储应用中不可串行化行为的动态预测分析
首个面向弱隔离数据存储应用的动态预测分析，通过SMT求解预测可行的不可串行化执行。
Quiver：在 Coq 中引导式溯因推断分离逻辑规约
提出 Quiver，在 Coq 中以用户规约草图为引导，溯因推断分离逻辑功能正确性规约并同时进行基础性验证。
交互式证明助手中的实时验证
在Coq中实现实时验证原型：逐行显示符号状态，并用diff形式表达循环不变式，边写代码边生成机器检查证明。
基于内在定义的可预测验证
提出用满足局部条件的 monadic maps 定义数据结构，实现可预测的验证。
V-Star：从程序输入中学习可见下推文法
提出 V-Star，用可见下推自动机主动学习，从样本输入推断程序输入文法的嵌套结构，并学习 S-表达式、JSON、XML。
Spacer 的归纳方法
用结构归纳重构 Spacer，统一 Spacer 与 GPDR，并分析其反驳完备性问题。
面向合成支持重构的规范化等价
提出基于规范化等价的程序合成框架，将直接风格代码重构为使用库组合子的等价代码。
面向已验证高层综合的 Hyperblock 调度
为 Vericert 实现经 Coq 验证的 hyperblock 调度器，通过翻译验证保证正确性，使生成硬件提速 2.1 倍。
一种轻量级的多语言代码转换语言
提出声明式多语言代码转换 DSL，通过组合、排序和流扩展轻量匹配替换，支持相互依赖的跨语言重构。
Allo：面向可组合加速器设计的编程模型
提出可组合编程模型 Allo，通过类型安全的定制原语自底向上组合硬件定制，支持跨函数整体优化。
通过注入真实世界代码增强编译器测试
提出 Creal，以保语义方式将真实项目函数注入种子程序，借真实代码提升随机生成器的表达能力来测试优化编译器。
面向量子纠错程序的符号执行
提出 QSE 符号执行框架与符号 stabilizer 态，高效分析量子纠错程序中的 Pauli 错误。
量子计算中控制流纠错的 T-复杂度代价
识别量子控制流抽象会以多项式增加 T-复杂度，提出代价模型与 Spire 程序级优化以恢复渐近高效性。
模块化与通用稀疏工作区的编译
提出一种编译器设计，自动检测稀疏散射并插入模块化稀疏中间工作区张量，以高效生成稀疏张量代数代码。
带冒险的流水线电路的模块化硬件设计
提出 hazard interfaces 将冒险引发的跨级依赖封装于接口中，实现含各类冒险的流水线电路模块化设计。
Descend：一种安全的 GPU 系统编程语言
提出 Descend，一种在类型系统中追踪所有权与生命周期、保证 CPU/GPU 内存安全并支持 GPU 层次化执行资源的系统编程语言。
KATch：面向 NetKAT 的快速符号验证器
为 NetKAT 网络规约语言设计新的符号自动机数据结构与算法，实现快速可扩展的等价性验证工具 KATch。
关联效应：面向效应式编程的灵活抽象
提出关联效应，使类型类能抽象其函数签名中的效应、由各实例指定具体效应，并在 Flix 中实现。
使用 Paramorphism 的递归程序合成
将递归程序合成拆分为固定递归结构的模板与非递归片段搜索，利用 paramorphism 简化并超越已有方法。
Jacdac：基于服务的嵌入式系统原型开发
提出并实现 Jacdac，用服务规格语言与单线总线将传感器/执行器抽象为可发现服务，便于嵌入式原型开发。
SPORE：结合对称性与偏序归约
首个可靠、完备且最优地结合对称归约与偏序归约的无状态模型检测器，并引入实现内部幂等操作对称性。
SpEQ：利用等价关系翻译稀疏代码
SpEQ 识别稀疏代码语义与存储前置条件，并将其正确翻译为高性能库或 DSL 调用。
任务完成：渐进安全性的圣杯
提出 λIFC★，在不牺牲类型引导分类与 no-sensitive-upgrade 下同时满足非干涉与渐进保证。
Superfusion：通过归纳合成消除中间数据结构
提出 superfusion，用归纳程序合成消除函数式程序中的中间数据结构，并以 ghost 函数分解草图填充问题。
松弛内存分离逻辑中线性一致性的证明配方
提出以对象修改序（OMO）为核心的证明配方，在 Coq 的 iRC11 分离逻辑中首次验证弱内存下多个并发对象的线性一致性。
面向托管运行时的乐观栈分配与动态堆化
提出静态分析引导的乐观栈分配与动态堆化机制，在托管运行时中更精确地栈分配对象并降低 GC 开销。
Daedalus：更安全的文档解析
提出安全解析器 DSL Daedalus，基于函数式解析组合子与流操作构造，可生成多语言安全解析器。
迈向可信的自动化程序验证器：形式化验证到中间验证语言的翻译
提出一种翻译验证方法，可为验证器前端到中间验证语言的翻译自动生成 Isabelle 可靠性证明。
命令式二叉搜索树的函数式本质
提出与命令式版本同速的 move-to-root、splay、zip 树函数式算法，并在 Coq/Iris 中机器验证等价性。
基于序列到树匹配的语法代码搜索：支持用不完整代码片段进行语法搜索
提出仅需词法分析、基于树自动机的序列到树匹配架构，使语法代码搜索可接受尚不可解析的不完整查询。
RichWasm：将安全、细粒度、共享内存互操作性下沉至 WebAssembly
提出 RichWasm，一种支持安全共享内存互操作并可编译到 WebAssembly 的富类型中间语言，并在 Coq 中证明类型安全。
NetBlocks：为高性能自定义主机网络协议栈 staging 布局
提出 NetBlocks DSL 与编译器，通过 staging 与布局定制层生成高性能、按需定制的网络协议栈实现。
共享变量并发的组合语义
为共享变量并发提出基于轨迹的指称语义，在标准单变量原语下获得无循环程序的全抽象性，并机器化验证。
一种用于规约量子网络的代数语言
提出基于 Kleene 代数的量子网络规约语言 BellKAT，并给出可靠完备的等式理论以验证网络协议。
模上下文敏感 α-等价性的哈希
提出上下文敏感 α-等价，证明其等价于互模拟，并给出 O(n log n) 哈希算法。
空间高效的多态渐进类型：大部分参数性
通过略微松弛参数性，给出支持参数多态的空间高效渐进类型强制转换演算与保持语义的翻译。
面向 Julia 的存在类型可判定子类型
证明 Julia 子类型不可判定，并提出将方法签名与值类型分层的限制以恢复可判定性。
Intel-x86 持久性语义下的验证
研究 Intel-x86 持久性语义下的可达性，给出持久性归约、一致性不可判定性与有界交替可判定性结果。
从批处理到流式：在线算法的自动生成
提出基于关系函数签名的离线算法到在线流式算法的自动合成方法，并实现 Opera。
不使用辅助量子比特编译条件量子门
提出一种无需辅助量子比特编译条件量子门的方案，门数仅为先前最佳方案的三分之一。
一族快速且内存高效的无锁与无等待内存回收方案
提出 Crystalline 系列非阻塞内存回收方案，同时实现高吞吐、高内存效率与完全无等待性。
流类型
提出流类型理论与核心演算 λ_ST，以顺序/并行组合和迭代算子刻画事件模式与并行结构，支持窗口、标点与分区等流式惯用法。
Wavefront Threading 实现有效的高层综合
提出硬件设计语言 Kanagawa，用 Wavefront Threading 执行模型融合 HLS 生产力与 RTL 硬件效率。
并发即时引用计数
提出 CIRC，将安全内存回收与引用计数结合，通过即时递归回收链式结构与即时递减，消除内存增长并缩小性能差距。
VESTA：基于语言运行时事件的功耗建模
提出仅依赖语言运行时事件的应用级功耗建模方法，精度与可解释性优于基于硬件性能计数器的方案。
将 qubit 电路编译为优化后的 qutrit 电路
提出 DARE，一个把 qubit 计算编译并优化为 qutrit 电路的编译器，通过分解与重写降低电路深度并提升保真度。
202383 篇 · 7(PLDI)
不动点迭代器的抽象解释及其在神经网络中的应用
提出仅抽象具体不动点的抽象解释框架与 CH-Zonotope 抽象域，在神经网络验证中显著提升速度、可扩展性与精度。
提示即编程：面向大语言模型的查询语言
提出语言模型编程（LMP）及查询语言 LMQL，把提示、脚本与输出约束统一，并编译为高效推理流程。
递归状态机引导的上下文无关语言可达性图折叠
提出由递归状态机引导的图折叠算法 GF，通过缩减输入图规模加速 CFL-reachability 程序分析。
合则更强：统一 Datalog 与等式饱和
egglog 将 Datalog 与等式饱和（EqSat）统一为定点推理系统，兼具增量执行、同余闭包与项抽取能力。
Lilac：一种面向条件概率的模态分离逻辑
提出 Lilac 分离逻辑，以分离合取刻画概率独立性，并基于 disintegration theory 引入条件概率模态。
深度神经网络（DNN）的架构保持可证明修复
提出架构保持的 V-polytope 可证明修复方法，仅改参数即可让 DNN 在指定凸多面体上满足规格，并实现工具 APRNN。
递归程序的自动化期望值分析
提出将前期望语义翻译为一阶约束的项表示，实现递归概率程序期望值的全自动推断。
概率编程语言的验证密度编译
提出 ProbCompCert：用 Coq 验证 Stan 子集概率编程语言编译器的关键遍，并发现 Stan 手册错误。
从带循环与条件化的概率程序到形式验证的采样器
提出经 Coq 形式验证的 Zar 编译器，将带循环与条件化的离散概率程序编译为正确采样器。
代码模型的离散对抗攻击
提出针对代码模型的语义保持程序变换离散对抗攻击，并给出对抗训练的理论基础与实现以提升鲁棒性。
基于时序不变量的模块化控制平面验证
提出 Timepiece，用逻辑时间路由模型与受时序逻辑启发的接口谓词，实现可靠可扩展的模块化控制平面验证。
神经网络的增量验证
提出增量且完备的 DNN 验证框架与工具 IVAN，避免网络更新后从头验证并显著加速。
程序重条件化（Program Reconditioning）：在发现与缩减编译器缺陷时避免未定义行为
提出程序重条件化，使含未定义行为且无检测工具的语言也能做程序生成、差分测试与用例缩减，在 GLSL/WGSL 编译器中发现 57 个缺陷。
WasmRef-Isabelle：一个经验证的 WebAssembly 单子解释器与工业级模糊测试预言机
在 Isabelle/HOL 中实现并机器化验证 WebAssembly 单子解释器，作为 Wasmtime 的模糊测试预言机，兼顾规范对应性与性能。
通过近似模型计数获得信息泄露边界
提出可靠（sound）的符号定量信息流分析，在路径探索不全与模型计数不精确时仍能给出信息泄露的上界与下界。
索引流：融合收缩程序的形式化中间表示
提出索引流：统一稀疏张量与关系代数融合收缩执行的形式化中间表示，证明正确性且性能可比专用系统。
面向已验证库的半自动化证明修复
提出首个高阶命令式函数的证明修复方法，在 Coq 中结合动态对齐和不变量综合，自动生成大部分证明并留下少量残余义务。
GPU 上基于搜索的正则表达式推断
提出正则表达式推断的枚举算法，以位向量矩阵紧凑编码搜索空间，并实现 CPU/GPU 版本，GPU 在困难基准上平均加速超千倍。
VMSL：面向通过 FF-A 通信的虚拟机机械化鲁棒安全性的分离逻辑
提出分离逻辑 VMSL，可模块化推理 FF-A hypercall ABI 上通信的虚拟机并机械化证明其鲁棒安全性。
PureCake：一个经验证的惰性函数式语言编译器
首个端到端机器验证的惰性函数式语言编译器，将 PureLang 编译到机器码并在 HOL4 中完成正确性证明。
基于自动机的量子电路验证与缺陷发现框架
提出基于树自动机的量子电路验证与缺陷发现框架，可验证大型电路并捕获注入缺陷。
Scallop：一种神经符号编程语言
提出 Scallop 语言，用基于 Datalog 的可微逻辑编程统一深度学习与符号推理。
Flux：面向 Rust 的液体类型
提出 Flux，将逻辑精化与 Rust 所有权结合，实现指针程序的易用类型验证与液态推断。
无上下文的上下文敏感：一种面向快速精确指针分析的 Cut-Shortcut 方法
提出 Cut-Shortcut，通过切割与捷径边在不使用上下文的情况下实现快速且精确的 Java 指针分析。
零知识证明中欠约束电路的自动检测
提出 QED 2，结合 SMT 求解与轻量级唯一性推断，自动检测零知识证明算术电路中的欠约束漏洞。
基于导数的、具有回溯语义的真实世界非回溯正则匹配
提出基于导数的非回溯正则匹配算法，支持锚点与计数并保持回溯语义，已在 .NET 7 实现并形式验证。
Iris-Wasm：WebAssembly 程序的鲁棒模块化验证
提出 Iris-Wasm，在 Coq/Iris 中为 Wasm 1.0 建立高阶分离逻辑，支持模块化验证与鲁棒安全。
利用 Rust 类型进行程序合成
提出首个面向安全 Rust 的按构造正确程序合成方法，用 Synthetic Ownership Logic 将类型约束与功能规约结合。
面向神经网络推理中非结构化稀疏的寄存器分块
提出稀疏寄存器分块，通过 unroll-and-sparse-jam 与数据压缩，为稀疏神经网络推理的 SpMM 内核提升寄存器复用并加速。
烤蛋糕的蛋糕：CakeML 中的动态计算
为已验证的 CakeML 编译器加入 Eval 原语，实现运行时代码求值与动态执行，并支持首个可验证的 LCF 风格定理证明器运行时环境。
通过迭代前向-后向抽象解释的归纳程序合成
提出交替迭代前向与后向抽象解释来剪枝搜索空间，显著提升归纳程序合成效果。
CRDT 收敛性的类型检查
提出 Propel 语言与类型系统，用类型检查自动验证 CRDT 实现所需的交换、结合、幂等等代数性质。
修复用于提取的正则表达式
提出首个基于编程示例的提取型正则合成与修复方法，支持反向引用与环视等扩展。
通过族多态实现可扩展的元理论机械化
提出基于族多态的语言设计，使证明助手能复用和扩展元理论机械化代码与证明。
证明与反驳函数式编程作业的等价性
用等价性检查自动证明或反驳函数式编程作业的正确性，并通过函数归纳与聚类提升鲁棒性和可扩展性。
CommCSL：使用抽象可交换性证明并发程序的信息流安全
提出基于抽象可交换性的关系并发分离逻辑 CommCSL，可自动验证并发程序的信息流安全，且不假设任何时序行为。
基于随机概率的概率编程
提出以随机估计密度比为核心的 PPL，首次同时支持边缘化、嵌套推断、随机控制流与可编程推断。
面向事务隔离级别正确性检查的动态偏序归约
提出覆盖 Read Committed、因果一致性、快照隔离与可串行化的动态偏序归约模型检测算法，完备、可靠、最优且多项式内存。
覆盖所有情况：测试输入生成器的基于类型验证
提出基于精化类型与 must 式欠近似推理的验证方法，确保测试输入生成器覆盖所有可接受输入。
Absynthe：抽象解释引导的程序合成
提出 Absynthe，一种语言无关、由用户自定义抽象语义引导的程序合成框架。
Don’t Look UB：揭示消除 Sanitizer 失败的编译器优化
提出差分测试框架 LookUB，发现 Clang 中 17 个消除 sanitizer 失败的优化，并挖出 20 个新 bug。
Performal：分布式系统延迟性质的形式化验证
提出 Performal，用形式化验证为真实分布式系统证明严格延迟上界，并发现性能缺陷。
为高效且鲁棒的优化合成 MILP 约束
提出基于 SyGuS 的方法，从布尔逻辑规约自动合成高质量 MILP 线性约束。
区域推断上下文中的并行性
为基于区域推断的编译器设计 fork-join 并行构造，并给出类型规则、动态语义、类型可靠性及效应推断算法。
合并归纳关系
提出合并共享索引的归纳关系的算法，生成等价合取关系，显著提升自动生成性能并简化 Coq 机械化证明。
超越回溯：细粒度并发分离逻辑中的连接
提出基于连接演算的多后继分离逻辑演算，在 Coq/Iris 中实现，减少回溯并自动验证细粒度并发程序。
CQS：一个形式化验证的公平且可中止同步框架
提出 CQS，用队列算法与 Coq/Iris 形式化证明实现公平、可中止同步原语，并在 JVM/Kotlin 协程中落地。
合成量子电路优化器
提出 QUESO，按量子设备自动合成带高概率正确性保证的量子电路优化器。
面向 C++ 与数据并行语言编译器的循环优化模糊测试
重实现 YARPGen，以静态避免 UB 和提升循环多样性来模糊测试编译器循环优化，发现 122 个 bug。
迹引导的递归函数式程序归纳合成
提出迹引导的归纳合成方法，用递归调用迹增强版本空间代数，从少量示例合成递归函数式程序。
Mosaic：面向张量代数的可互操作编译器
提出可互操作的稀疏张量代数编译器 Mosaic，通过调度 API 将子表达式绑定到外部函数并自动融合生成其余代码。
cuCatch：一种高效捕获 CUDA 应用程序内存安全违规的调试工具
提出面向 CUDA 的内存安全检测工具 cuCatch，用编译器插桩与驱动支持低开销捕获时空违规。
线性时间内的可靠动态死锁预测
提出 sync-preserving 死锁概念，并给出线性时间、可靠且高精度的动态死锁预测算法。
ImageEye：基于程序合成的批量图像处理
提出神经符号DSL与程序合成方法，从用户演示自动生成细粒度批量图像编辑程序。
CryptOpt：面向密码原语的随机程序搜索与验证编译
首个将高层密码函数式程序编译为汇编的流水线，通过随机搜索与 Coq 机器化证明，生成比 GCC/Clang 更快的代码。
C11 风格内存模型的最优 reads-from 一致性检查
为 C11 风格内存模型（RC20、RA、SRA/WRA、Relaxed）的 reads-from 一致性检查给出最优算法与复杂度下界。
面向硬件反编译的循环重卷
提出硬件反编译问题，并用克隆检测与程序合成技术将网表中的重复逻辑重卷为 HDL 循环。
复合内存模型
提出组合式操作模型，刻画不同一致性模型设备融合后的复合内存模型，并以 x86TSO/PTX 为例验证。
公平操作语义
提出 FOS，把任意公平性概念编码为操作语义，并用资源代数实现线程局部公平性推理。
flap：一种融合词法分析的确定性解析器
提出确定性 Greibach 范式，将词法与语法分析融合，实现无 token 流的高效确定性解析器组合子库 flap。
面向计算机辅助设计的基于谱系的引用 DSL
提出基于谱系的引用DSL，将CAD引用作为一等构造，安全表达参数变化下的几何元素选择。
通过 Lambda 集特化实现更好的去函数化
提出 Lambda Set Specialization，首个不受限特化去函数化技术，并用类型系统与机器化证明支撑。
用于文件格式解析的区间解析文法
提出区间解析文法 IPG，为每个文法符号附加输入区间与属性，从而声明式地刻画文件格式中的上下文相关模式并自动生成解析器。
在分离逻辑中嵌入后见推理
提出时间插值证明原则，在并发分离逻辑中自动化后见推理，验证并发数据结构线性一致性。
带效应的高效并行函数式编程
提出支持纠缠与任意突变的技术，使并行函数式语言兼顾安全与性能。
通过 Promising 中间表示让弱内存有序
提出按序弱内存并发模型，通过 source/IR 分离支持非原子访问与单线程优化，并在 Coq 中验证到 Armv8 的映射。
基于程序草图的单像素对抗攻击
提出 OPPSLA，利用程序草图合成与随机搜索生成单像素对抗样本，显著减少查询并提升成功率。
面向布局引擎的冲突驱动合成
提出 Medea 框架，通过冲突驱动的程序合成自动生成正确且高效的增量布局引擎。
Memento：持久内存中可检测可恢复性的框架
Memento 是一个面向持久内存并发数据结构的通用高性能框架，用时间戳恢复策略实现可检测可恢复性并给出形式化证明。
参数化代数协议
提出参数化代数协议，以代数数据类型风格统一并扩展会话类型，实现线性时间类型检查。
带同步的响应式并行
通过类型系统与动态优先级调整，防止互斥锁和条件变量使用中的优先级反转，实现响应式并行。
面向编程语言实现一致性测试的特征敏感覆盖
提出特征敏感与特征调用路径敏感覆盖准则，提升语言实现一致性测试生成质量并发现大量 JS 实现缺陷。
Taype：一种策略无关的不经意计算语言
提出Taype语言，将安全策略与程序逻辑解耦，并首次实现不经意代数数据类型与磁带语义。
面向高效机密性保护的广义基于策略的非干扰性
提出机制无关的保密数据分析语言，以格标签、可表达安全策略和广义非干扰类型系统自动高效组合多种安全机制。
基于 region 的类型多态程序的垃圾回收安全性
指出区域推断对多态高阶程序的 GC 安全性缺陷，提出带 GC 效应的区域类型系统并修复实现。
切蛋糕：一种公平分配语言
提出公平分配领域专用语言 Slice，将协议编译为逻辑约束并调用求解器自动验证无嫉妒性。
跨外部函数接口（FFI）回收循环垃圾：谁拿走最后一块蛋糕？
提出 Refgraph GC，跨 FFI 回收两个托管语言间的循环垃圾，且只需修改一方运行时。
Psym：分布式系统的高效符号探索
提出 Psym，用细粒度规范配置表示在符号探索中同时避免状态、交错及状态更新计算的冗余，提升分布式系统验证可扩展性。
基于时间线类型的模块化硬件设计
Filament 用时间线类型静态描述并检查硬件的时序与结构约束，实现模块安全组合与正确流水线化。
面向安全间歇计算的类型系统
提出首个面向 Rust 的安全间歇计算类型系统 Curricle，用信息流与类型限定符表达并检查幂等性要求。
HEaaN.MLIR：面向快速环基同态加密的优化编译器
提出 HEaaN.MLIR 编译器与 Poly/ModArith IR，跨多项式运算优化，最高实现 4.55 倍提速。
带重试编排的可靠 Actor
提出基于 Actor、重试编排与尾调用的云容错编程模型，并形式化与实现验证。
带依赖类型的去函数化
首次为依赖类型语言形式化定义去函数化翻译，并证明其可靠性与类型保持。