ICSE 2291 ASE 2141 FSE 1566 ASPLOS 1219 LMCS 1020 OOPSLA 737 LICS 679 ISSTA 617 POPL 609 ICFP 374 PLDI 369 TOPLAS 199 JFP 172 arXiv 预印本 5
标签：机器学习与程序语言（共 3066 篇，按优先级展示前 200）
增强静态分析以进行实用缺陷检测：一种 LLM 集成方法
提出 LLift，将静态分析与 LLM 结合，用于检测 Linux 内核中的未初始化使用缺陷。
LLM 遇上界模型检测：神经符号循环不变式推断
提出“查询-过滤-重组”策略，用 LLM 生成候选循环不变式、以有界模型检测筛选谓词并组装，再由 SMT 求解器校验。
无循环展开的有界模型检测中由LLM生成的循环不变式
用LLM生成循环不变式并由一阶定理证明器校验，从而在CFG层面消除循环，扩展有界模型检测对无界循环程序的验证能力。
AutoVerus：为 Rust 代码自动生成证明
提出 AutoVerus，用 LLM 智能体网络自动为 Rust 代码生成 Verus 正确性证明，90%+ 任务成功。
Cobblestone：一种自动化形式验证的分治方法
Cobblestone 用 LLM 分治合成 Coq 证明：拆分已验证子目标并迭代，保持可靠性，自动化形式验证。
TaintP2X：检测 LLM 集成应用中的污点式 Prompt-to-Anything 注入漏洞
提出静态污点分析框架 TaintP2X，将 LLM 输出视为污点源，检测 LLM 集成应用中的 P2Xi 注入漏洞。
基于大语言模型的证明自动化
提出 PALM：让 LLM 先生成证明，再用符号方法迭代修复低层错误，大幅提升 Coq 形式证明自动化成功率。
机器生成、机器检查的验证编译器证明（经验报告）
用 Claude Code 智能体从零机械化 CertiRocq 中 ANF 变换的语义保持证明，产出约 6000 行 Rocq 证明，耗时 94.5 小时。
面向贝叶斯程序分析的抽象选择学习
提出基于学习的数据驱动框架，为贝叶斯程序分析自动选择抽象，以提升其泛化能力。
KVerus：面向 Rust 代码的可扩展且鲁棒的形式化验证证明生成
提出 LLM 辅助的 Verus 证明生成工作流 KVerus，用动态知识库支持仓库级跨文件证明生成与修复。
神经符号模块化精化类型推断
提出神经符号 agent LHC，用 LLM 自动生成整包精化类型标注并由 LiquidHaskell 验证，大幅降低形式验证标注成本。
智能体程序验证中的自动化引理发现
提出 LLM 智能体 LemmaNet，通过程序语义理解离线合成与在线适配辅助引理，自动完成演绎验证中的 VC 证明。
DepRadar：面向深度学习库上下文感知缺陷影响分析的智能体协同框架
DepRadar 用多个专门化智能体协同静态分析与领域规则，自动判定深度学习库缺陷是否影响下游程序。
Fun2spec：大规模代码契约合成
首个工业级工具，引导 LLM 合成带量词的一阶逻辑 C++ 规范，准确率达 85%。
通过对局部推理错误的反馈引导基于 LLM 的循环不变式合成
通过形式化验证 LLM 的推理步骤并定位局部逻辑错误，为其循环不变式合成提供建设性反馈，显著提升成功率。
贝叶斯程序分析引导的 LLM 告警消解
提出由贝叶斯程序分析引导 LLM 判断中间事实并剪枝依赖告警的静态分析告警消解框架，兼顾质量与 token 开销。
LLM 增强的程序分析：迈向实用且可扩展的缺陷检测
提出用 LLM 增强静态分析，通过神经-符号混合框架提升缺陷检测的精度与可扩展性。
当 AllClose 失效时：深度学习程序的舍入误差估计
提出 Render，用动态区间算术与舍入误差分析估计最大舍入误差，区分可接受误差与实现缺陷。
SAIL：使用大语言模型构建可靠的抽象解释器
提出 SAIL 框架，利用 LLM 自动合成全局可靠的抽象变换器，将任务形式化为约束优化并用不可靠度代价函数指导搜索。
AutoCodeRover：自主程序改进
结合 LLM 与基于 AST 的代码搜索及频谱故障定位，自动解决 GitHub issue 并生成补丁。
检测神经网络架构中的数值缺陷
首次面向神经网络架构，提出基于抽象解释的静态分析以检测数值缺陷。
SpecGen：基于大语言模型的形式化程序规约自动生成
SpecGen 利用 LLM 对话式生成并变异筛选可验证的形式化程序规约，在 385 个程序上成功生成 279 个可验证规约。
HoarePrompt：面向自然语言中程序正确性的结构化推理
提出 HoarePrompt，将最强后置条件与 k-归纳引入 LLM，用自然语言推理程序对需求的正确性。
在真实工业环境中检测 TensorFlow 程序缺陷
通过大规模实证研究并提出基于约束的 ShapeTracer，检测工业 TensorFlow 程序的形状相关缺陷。
基于大语言模型的语义增强间接调用分析
提出 SEA，用 LLM 生成间接调用与目标函数的语义摘要来过滤虚假目标，提升静态分析精度。
HARP：跨计算图与宿主 Python 代码的整体分析
HARP 通过跨计算图与宿主 Python 代码的整体分析来重构 ML 程序，平均加速 2.07 倍。
大语言模型驱动的符号执行
提出基于路径分解的 LLM 符号执行方法，用代码表示泛化路径约束让 LLM 直接推理，并实现轻量、语言无关的 AutoBug 引擎。
基于LLM资源导向意图推断的静态资源泄漏检测增强
提出InferROI，用LLM推断资源获取/释放/可达性验证意图，再结合两阶段静态分析提升资源泄漏检测。
Laurel：用大语言模型解除自动验证的阻塞
Laurel 利用大语言模型自动生成 Dafny 断言，通过错误定位与代码库示例提示，减少验证器所需人工提示。
通过溯源分析保障 LLM 智能体免于失准
提出基于溯源分析的形式化框架与 ProvenanceGuard 流水线，在工具调用执行前检测 LLM 智能体的失准行为。
PredicateFix：用桥接谓词修复静态分析告警
利用分析规则中的谓词检索关键样例，构建 RAG 流水线自动修复静态分析告警，显著提升 LLM 修复正确率。
迈向更精确的 Linux 内核污点式缺陷检测静态分析
提出 BugLens，用结构化 LLM 推理对静态分析告警进行后精化，将 Linux 内核污点式缺陷检测精度从 0.10 提升至 0.72。
Rango：面向自动化软件验证的自适应检索增强证明
提出 Rango，用检索增强的微调 LLM 在 Coq 中自动识别相关前提与相似证明，实现全自动证明合成。
结合静态分析与贝叶斯推断的鲁棒资源界
提出 Hybrid AARA，将类型化静态资源分析与贝叶斯推断融合，得到统计可靠且更鲁棒的最坏情况资源界。
LLM 辅助的内存安全
提出 MSA 框架，用 LLM 结合轻量静态分析将 C 代码移植到 CheckedC，自动推断注解并重构代码。
不动点迭代器的抽象解释及其在神经网络中的应用
提出仅抽象具体不动点的抽象解释框架与 CH-Zonotope 抽象域，在神经网络验证中显著提升速度、可扩展性与精度。
Planning to Hammer：面向 Rocq 证明自动化的难度感知分解
Quarry 将证明规划与执行分离，用 LLM 提出分解并由难度模型排序，递归调用 CoqHammer 提升 Rocq 证明自动化。
LPO：利用大语言模型发现遗漏的窥孔优化
结合大语言模型与形式化验证，闭环自动发现 LLVM 中遗漏的窥孔优化。
Refty：基于细化类型的深度学习模型静态检查
提出基于细化类型的工具 Refty，用 SMT 求解算子约束，在运行前静态检测深度学习模型的类型错误。
通过软证据在贝叶斯程序分析中融合形式信息与非形式信息
将 Datalog 分析概率化，用神经网络把变量名等非形式信息编码为软证据，以改进报警排序。
3DGen：AI 辅助生成可证明正确的二进制格式解析器
提出 3DGen，用 AI 智能体将 RFC 与示例转成 3D 规约，并综合出可证明正确的 C 解析器。
AgenticTyper：使用智能体 AI 对遗留软件项目进行自动类型标注
提出基于 LLM 智能体的自动化类型标注系统，通过迭代纠错与转译对比保持行为，20 分钟解决 633 个类型错误。
LLM 辅助的高保障 C 程序合成
提出 SynVer，用两个 LLM 分别合成 C 程序候选并生成 Rocq/VST 正确性证明，实现高保障 C 程序合成。
CoqPilot：基于 LLM 生成证明的插件
提出 CoqPilot：一个 VS Code 插件，结合 LLM 与传统方法自动填补 Coq 证明空洞，并提供基准测试平台。
迈向命令式深度学习程序到图执行的安全自动化重构
提出基于命令式张量分析的自动化重构方法，安全地将深度学习 eager 代码迁移到图执行。
大语言模型辅助的部分程序依赖分析
提出利用大语言模型辅助部分程序依赖分析，缓解不完整代码片段上精度与召回率的权衡。
SpecPylot：基于大语言模型的 Python 规约生成
提出 SpecPylot，用 LLM 生成 icontract 规约，并借助 CrossHair 符号执行验证与反例驱动迭代修正。
面向 Move 程序的智能体式规约生成器
提出 Msg，面向 Move 智能合约自动生成可验证规约，84% 函数成功，可验证子句提升 57%。
基于事实对齐与模板约束的 LLM 静态分析器规则增强
提出 RuleRefiner，用 LLM 多阶段精化静态分析器检测规则，从根本上减少误报与漏报。
规划大型语言模型以静态检测代码片段中的运行时错误
提出 Orca，让 LLM 自主规划沿控制流图预测执行代码片段，从而静态检测运行时错误。
智能体软件系统的过程中心分析
提出 Graphectory 图编码智能体轨迹的时序与语义关系，实现以过程为中心的分析与在线监控，提升问题解决率。
带天使式假设的开放程序内存安全验证
提出 Seeker，用 LLM 挖掘惯用模式并实例化为天使式假设来补全缺失代码，以高精度区分开放程序内存安全误报与真实缺陷。
仅凭测试能否合成形式规约？
用 LLM 仅从测试代码与动态执行轨迹（黑盒）推断 JML 形式规约，并以有界模型检验迭代精化。
利用系统级观测为定量验证中的模型参数贝叶斯学习提供信息
提出 EPIK，用可直接观测的系统级属性引导贝叶斯先验，从而更准确地对模型转移参数学习并验证难以测量的定量性质。
面向可满足性模理论、Oracle 与自然语言的 LLM 辅助不可满足性证明
首个能为含闭盒函数调用的 SMT 公式生成不可满足性证明的求解器，借助 LLM 从自然语言文档猜想辅助引理。
数据感知的静态分析：利用数据特征改进机器学习代码中的语义错误检测
提出数据感知的静态分析，结合数据流、控制流与 API 契约，在编码阶段检测机器学习代码的语义错误。
SpecGuru：层次化LLM驱动的API指向规约生成与自验证
提出层次化LLM驱动并自验证的API指向规约生成方法，缓解第三方API复杂语义、语法与边界情况带来的静态分析困难。
基于智能体所有权分析与修复模式验证的项目级资源泄漏检测
提出首个集成 LLM 智能体的项目级资源泄漏检测框架 AROP，通过元数据筛选、智能体识别与数据流验证降低误报。
通过 SMT 求解检查无监督学习中的非确定性与不一致性
提出 Ocelot，将无监督学习实现中的非确定性与不一致性检查归约为 Z3 可满足性求解，并生成见证数据集以复现错误。
HarnessLLM：用大语言模型生成 Rust 验证 harness
提出 HarnessLLM，从既有测试套件自动抽取调用场景并用 LLM 增量生成、迭代修复 Rust 验证 harness，检出 6 个真实内存安全缺陷。
PAGENT：学习修补软件工程问题修复智能体
系统研究 LLM 问题修复智能体的失败模式，并提出类型感知的后处理代理 PAGENT 修复错误补丁。
ACTaint：基于智能体的智能合约访问控制漏洞污点分析
提出基于LLM多智能体的污点分析系统ACTaint，用于检测Solidity智能合约访问控制漏洞。
面向安全最小化的大语言模型
提出 SafeMin，将 LLM 与 SMT 求解器协同用于不可行字符串约束系统的安全最小化与 MUS 计算。
Beer：通过探索-利用实现贝叶斯程序分析中的交互式告警消解
将探索-利用权衡引入贝叶斯程序分析，利用告警结构相关性提升交互式告警排序与消解效率。
1001 行代码的故事：潜在运行时错误引导的规约合成用于验证大规模程序
提出 Preguss，以潜在运行时错误引导静态分析与 LLM 分治合成过程间规约，实现千行级程序的高自动验证。
将路径重构为逻辑：面向漏洞检测的语义分段方法
SEVDF 用污点分析提取候选路径、再由 LLM 做语义分段与可行性确认，高效检测 C/C++ 路径敏感漏洞。
用于神经网络认证的抽象域
提出结合浮点多面体与区间的抽象域 DeepPoly，实现对深度神经网络可扩展且精确的认证。
Baldur：使用大型语言模型进行整体证明生成与修复
用微调大语言模型一次性生成完整证明，并借助失败尝试与错误信息修复，提升自动形式化验证能力。
用大语言模型辅助静态分析：一项 ChatGPT 实验
通过精心设计的函数行为与函数摘要提问，用 LLM 有效剔除静态分析工具产生的误报。
学习减少分析型缺陷检测器中的误报
用 Transformer 模型识别静态分析误报，将分析精度提升 17.5%。
Notebook 中的数据泄漏：静态检测与更佳流程
提出静态分析检测数据科学 Notebook 中训练/测试数据泄漏，并在十万级公开 Notebook 上验证其普遍性。
基于概率推断的智能调试
提出概率推断调试技术，融合人类推理与程序语义以定位最可能故障语句。
学习静态分析告警的概率模型
提出 BayeSmith，自动学习静态分析告警概率模型的结构与权重，以更好排序真实缺陷并减少误报。
自动化程序精化：用精化演算引导并验证代码大语言模型
提出 Refine4LLM，用精化演算自动引导并验证 LLM 生成代码，在保证正确性的同时提升自动化程度。
用于 Clarke 雅可比矩阵静态分析的对偶数抽象
提出对偶数抽象域，可靠过近似 Clarke 雅可比，并实现 DeepJ 分析非光滑神经网络的 Lipschitz 鲁棒性与优化景观。
Locus：面向定向模糊测试的 Agentic 谓词合成
提出 Locus，用智能体合成中间状态谓词引导定向模糊测试，平均加速 41.6 倍并发现 9 个新漏洞。
基于学习的静态程序切片方法
提出 NS-Slicer，用预训练语言模型预测完整与不完整代码的静态切片，并用于漏洞检测。
Marble：面向 RNN 深度学习系统的定量鲁棒性分析
提出 Marble，通过概率抽象与迭代精化对真实 RNN 深度学习系统进行定量鲁棒性分析。
使用语言模型的类型约束代码生成
提出类型约束解码：用前缀自动机与可居留类型搜索保证 LLM 生成代码良类型，编译错误减少过半。
高阶自动微分的抽象解释的通用构造
提出一种通用构造，可将高阶自动微分的抽象解释归约为对实值直线程序的抽象推理。
ExAIS：神经网络框架的正确性规约与可执行语义
用 Prolog 为 TensorFlow 几乎所有层建立可执行语义，并据此实现 fuzzing 与模型验证。
LLM 辅助的安全协议验证自动建模
提出用 LLM 分阶段自动从自然语言文档生成安全协议的符号模型，并用可证可靠的模型变换保证正确性。
MalSkills：通过神经符号推理检测智能体供应链中的恶意技能
提出神经符号检测框架 MalSkills，从异构构件中推理识别 LLM 智能体供应链中的恶意技能，F1 达 93%。
基于 LLM 引导策略选择的自适应证明精化
提出 Adapt 框架，用 LLM 引导的决策器动态选择证明精化策略，显著提升定理证明的自动化成功率。
连接自然语言与形式规约——使用LLM通过层次语义分解自动将软件需求翻译为LTL
提出Req2LTL，用LLM分层语义分解与规则合成将自然语言需求自动翻译为LTL。
面向代码优化的具体类型推断：结合机器学习与 SMT 求解
提出结合机器学习与 SMT 求解的具体类型推断，无需类型标注即可优化动态类型 Python 代码。
基于多模态验证器的可认证程序合成
提出基于 Lean 多模态验证器 Velvet 的分阶段 agent 流水线 LeetProof，实现从自然语言到程序、规格与机器可检验证明的可认证合成。
自动化需求形式化：使用 LLM 与低复杂度区分迹进行语义验证
提出 ARTEMIS，用 LLM 将自然语言需求经结构化中间表示译为时序逻辑，并用低复杂度区分迹把人工验证开销对数级削减。
迈向 SMT 辅助的证明导向编程的神经合成
构建 60 万行 F* 程序与证明数据集，并探索用微调小模型和检索增强进行类型导向的程序与证明合成。
编写你自己的代码检查器：一种基于 LLM 的自动化测试驱动检查器开发方法
提出 AutoChecker，仅凭规则描述与测试套件，用 LLM 迭代生成代码检查器，平均测试通过率达 82.28%。
从深度学习模型中推断数据前置条件以实现部署中的可信预测
提出 DeepInfer：将训练好的 DNN 抽象为可做最弱前置条件推理的表示，从输出后置条件推断输入前置条件，以判定部署预测的可信性。
PAT-Agent：面向模型检测的自动形式化
提出 PAT-Agent，结合 LLM 规划、代码生成、PAT 模型检测与反例修复，实现自然语言到可验证形式模型的端到端自动形式化。
面向精确类型错误检测的大语言模型反射式单元测试生成
提出 rTED，用类型约束分析与反射验证引导 LLM 生成单元测试，精准检测 Python 类型错误并降低误报。
面向代码智能体检索的 TypeScript 仓库索引
基于 TypeScript Compiler API 实现 abcoder-ts-parser，直接复用编译器 AST 与语义信息，为代码智能体高效构建函数级代码索引。
AgenticSCR：面向未成熟漏洞检测的自主智能体安全代码审查
提出带安全语义记忆的智能体代码审查器，在早期漏洞检测中显著优于静态LLM、多智能体与SAST工具。
REAP：从交互式生产使用中自动整理编码智能体基准
提出 REAP 自动化流水线，从真实开发者-智能体会话构建可执行、可复现的生产分布基准 Harvest。
RFCAudit：用于审计协议实现是否符合 RFC 规范的 AI Agent
提出基于 LLM 的自主审计 agent，检查协议实现与 RFC 规范的一致性，在六个真实实现中发现 47 个功能缺陷。
Parf：面向抽象解释的自适应参数精化
提出全自动框架 Parf，将静态分析器外部参数建模为随机变量并增量精化，在时间预算内显著降低误报。
DafnyRAG：一个检索增强与验证驱动的 Dafny 代码自动修复工具
提出结合形式验证反馈与检索增强生成来迭代修复 Dafny 代码并提升形式规约准确性的工具。
调用图剪枝真的有效吗？
通过构建新数据集与多框架评估，发现调用图剪枝在提升精度的同时造成显著覆盖率损失，并揭示原有评估方法的缺陷。
通过神经符号约束学习测试深度学习库
提出神经符号约束学习技术 Centaur，从种子输入学习 DL API 约束，用 SMT 生成有效多样测试并发现新缺陷。
AutoCodeRover：面向 SonarQube 问题的智能体程序修复
将 AutoCodeRover 程序改进智能体适配为 SonarQube 修复智能体，自动为静态分析问题生成补丁并接入 PR 审查流程。
带局部结构的信念传播及其在程序分析中的应用
提出利用局部结构编码因子加速环状信念传播，并用于程序分析。
基于 DSL 源代码转换的自动化深度学习优化
提出 Adopter，用 DSL 表达 DL 模型与转换规则，自动将 DL kernel 集成到模型中，提升精度召回与训练效率。
Proofs Promptly：用 AI Agent 进行面向证明的编程（经验报告）
经验报告：配备证明助手与 CLI 的 AI Agent 可自动产出数千行机器检验证明代码，把人类专家的工作压缩到给定问题描述与审查规约。
DR.FIX：在工业规模下自动修复数据竞争
提出 Dr.Fix，结合 LLM 与程序分析在 Go 中自动修复数据竞争，并在 Uber 大规模部署验证。
保证浮点神经网络分类一致性的量化
提出CoMPAQt用MILP验证量化网络分类不一致性，并给出保证或近似保证与浮点网络分类一致的纠正机制。
面向机器学习内核的符号化基本块剖析
提出符号化程序剖析，用输入相关的符号公式代替动态插桩计算 ML 内核基本块计数，中位加速约 1.5 万倍。
AI 智能体中徒劳循环（futile cycle）检测的无监督方法
提出智能体执行轨迹中“徒劳循环”的概念，并用结构加语义的无监督混合方法检测，F1 达 0.72。
It Takes Two to Entangle：分布式机器学习模型的细化检查
提出 Entangle，用迭代重写静态检查分布式模型是否细化顺序模型，以定位分布式 ML 中的 bug。
面向需求驱动代码验证的AI多智能体系统及其工业部署
提出并工业部署ARC-V多智能体系统，用LLM实现需求驱动的代码验证与早期缺陷发现。
Holmes：面向工业规模混合语言移动崩溃的多模态智能体诊断
多智能体系统 Holmes 利用多模态运行时信号，在无复现条件下对工业级混合语言移动崩溃做根因定位。
LineBreaker：用大语言模型发现 Token 不一致性缺陷
首次系统评测 LLM 检测 Token 不一致性缺陷的能力，并提出级联检测系统 LineBreaker，提升精度、召回与可扩展性。
STaint：用LLM辅助的双向静态污点分析检测PHP应用中的二阶漏洞
提出LLM辅助的双向静态污点分析方法STaint，精确建模自定义数据库读写，检测PHP二阶漏洞。
Spec2Code：将协议规范映射到函数级代码实现
提出首个LLM驱动的函数级协议规范到代码映射框架，支持细粒度一致性检查并发现真实不一致。
用于检测变量误用的代码理解 Linter
提出基于代码语言模型的代码审查工具，检测 Python 变量误用并生成修复建议。
面向 Isabelle/HOL 神经定理证明的极简证明语言
提出极简证明语言 Minilang，并翻译 Isar 语料微调 LLM，以提升 Isabelle/HOL 神经定理证明性能。
Expecto：从自然语言描述中抽取形式化规约以构建可信赖的 Oracle
Expecto 用神经符号方法从自然语言意图中自顶向下模块化合成 DSL 形式规约，作为可信赖的规约预言机。
RunbookFX：面向可执行事故诊断与缓解的类型与效应安全的 LLM 合成
提出类型化函数式 DSL RunbookFX，用乘积效应代数把事故响应安全分解为风险、能力、回滚三维，并以 Coq 机化证明保障 LLM 合成程序的安全性。
基于编译器引导大语言模型归约分析的输入中心代码优化
结合编译器与LLM的归约分析自动识别关键输入特征，将输入识别时间缩短44至450倍，支撑输入中心优化。
PyTorch 2：通过动态 Python 字节码变换与图编译加速机器学习
PyTorch 2 的 torch.compile 借助动态字节码变换捕获计算图并编译，在真实模型上取得显著加速。
InferFix：基于大语言模型的端到端程序修复
提出 InferFix，结合静态分析器与检索增强的微调 LLM，实现安全与性能缺陷的端到端自动修复。
面向深度神经网络的 Concolic 测试
提出首个面向深度神经网络的Concolic测试方法，以线性算术表达测试需求，提升覆盖率并发现对抗样本。
估算深度学习模型的 GPU 内存消耗
提出 DNNMem，一种在运行前精确估算深度学习模型 GPU 内存消耗的解析式工具。
提示即编程：面向大语言模型的查询语言
提出语言模型编程（LMP）及查询语言 LMQL，把提示、脚本与输出约束统一，并编译为高效推理流程。
WhiteFox：由大语言模型赋能的白盒编译器模糊测试
提出首个利用 LLM 与编译器源码信息的白盒编译器模糊测试器 WhiteFox，用于检测深度学习编译器的深层逻辑缺陷。
受数据流分析启发的深度学习用于高效漏洞检测
提出 DeepDFA，一种受数据流分析启发的图学习框架与嵌入技术，实现高效且有效的漏洞检测。
SWE-Debate：面向软件问题解决的竞争性多智能体辩论
提出竞争性多智能体辩论框架 SWE-Debate，通过故障传播轨迹与三轮辩论实现更统一的缺陷定位与补丁生成。
Fairify：神经网络的公平性验证
提出基于 SMT 的神经网络个体公平性验证方法，通过输入划分与神经元剪枝实现可扩展的认证与反例生成。
ReluDiff：面向相关神经网络的差分验证
提出 ReluDiff，对两个相关神经网络进行差分形式验证，通过前向区间分析与反向梯度精化证明输出差异性质，显著加速验证。
机器学习云 API 是否被正确使用？
人工研究 360 个使用 ML 云 API 的开源应用，发现 70% 存在误用，归纳出 8 类反模式并实现自动检查器。
提示调优的代码语言模型作为静态类型部分代码类型推断的神经知识库
将类型推断重构为完形填空任务，用提示调优的代码掩码语言模型作为神经知识库实现模糊类型推断。
迈向 LLM Agent 可验证安全的工具使用
结合 STPA 危害分析与能力增强 MCP，为 LLM Agent 的工具调用提供形式化安全护栏。
它们有多有效？探索基于大语言模型的模糊测试驱动器生成
首个系统性实证研究：大规模评测 LLM 生成 fuzz driver 的有效性、提示策略与工业界差距。
DeepStability：深度学习中的数值稳定性问题与解决方案数据库
分析 PyTorch 与 TensorFlow 的数值不稳定问题，建立首个深度学习数值稳定性问题与解决方案数据库。
理解深度学习系统中的性能问题
首个系统研究 TensorFlow/Keras 深度学习系统性能问题的症状、根因与阶段，并构建基准与静态检查器 DeepPerf。
多样性驱动的自动形式化验证
提出 Diva，通过训练多样化的证明脚本模型并结合搜索，显著提升 Coq 定理的自动证明率。
Relax：面向端到端动态机器学习的可组合抽象
提出 Relax 编译器抽象，以跨层表示与一等符号形状标注优化端到端动态形状机器学习负载。
面向 DNN 的基于 PAC 模型学习的实用鲁棒性分析
提出基于 PAC 模型学习的黑盒框架，将模型学习融入 DNN 局部鲁棒性分析，提升实用性与可扩展性。
NeuroDiff：面向前馈 ReLU 神经网络差分验证的符号化细粒度近似
提出 NeuroDiff，用新凸近似与符号变量细粒度界定两个 ReLU 网络输出差，实现高精度快速差分验证。
面向 Python 的生成式类型推断
提出 Typegen，将静态分析步骤转为思维链提示，实现少样本、可解释的 Python 类型推断。
PYEVOLVE：自动化 Python 机器学习系统中的频繁代码变更
提出数据流/控制流感知的变换规则推断引擎，自动挖掘、推断并移植 Python ML 系统中的频繁代码变更。
通过全局分析与张量表达式优化深度学习推理
提出 DNN 编译器 Souffle，以张量表达式构建全局依赖图并做跨算子边界的优化，显著加速推理。
大型预训练语言模型赋能的 SMT 求解器验证
提出 LasT，用重训练-微调与数据增强驱动 LLM 生成 SMT 公式来模糊测试求解器，发现 65 个真实缺陷。
用类型化洞为大型语言模型提供静态上下文
将LLM代码生成集成到Hazel的带类型洞环境，通过语言服务器提供静态类型与绑定上下文，显著提升补全质量并证明类型定义上下文最有效。
SpecRover：利用 LLM 进行代码意图提取
提出 SpecRover，一种基于 LLM 智能体的迭代规约推断与代码搜索工作流，显著提升自动程序修复效果并降低成本。
面向循环不变式学习的区间反例
提出区间反例以提升循环不变式黑盒学习中的样例质量，减少约束查询次数。
神经网络的区间通用逼近
提出区间通用逼近定理，并证明构造精确区间分析神经网络本质困难。
揭示并检测深度学习 API 的误用
首个针对 TensorFlow 与 PyTorch 的深度学习 API 误用大规模实证研究，并提出基于 LLM 的检测与修复方法 LLMAPIDet。
ChopChop：一个对语言模型输出进行语义约束的可编程框架
提出首个可编程框架 ChopChop，通过对程序前缀的可实现性做共归纳分析，对语言模型生成施加语义约束。
面向 ML 赋能系统安全的感知契约
提出感知契约，用于刻画神经感知误差并保障基于视觉感知的控制系统安全。
DyCL：通过程序重写与图优化的动态神经网络编译
提出 DyCL，通过程序重写和图优化使现有深度学习编译器成功编译动态神经网络，并提升执行性能。
LLM Agent 技能如何泄露你的凭证：一项实证研究
首次大规模实证研究 LLM agent 技能的凭证泄露，归纳出 10 类泄露模式，并揭示 fork 分发使修复失效。
面向数值缺陷的深度神经网络架构可靠性保障
提出 RANUM，首个既能用失败测试确认 DNN 潜在数值缺陷可行性、又能自动生成修复的方法，在 63 个真实架构上优于现有方法。
基于LLM的智能体方法用于自动化代码设计问题定位
提出多智能体框架LOCALIZEAGENT，利用LLM将程序分析结果转为自然语言摘要并定位代码设计问题。
通过学习激进状态剪枝策略提升符号执行效果
提出 HOMI，用学习驱动的激进状态剪枝只保留少量有前景状态，显著提升符号执行的覆盖率与缺陷发现能力。
SoD2：静态优化动态深度神经网络执行
提出 SoD2 框架，通过秩与维度传播静态确定动态 DNN 算子形状，实现融合代码生成、执行规划与内存分配优化。
识别 Stack Overflow 代码片段中的智能合约安全问题
提出 SOChecker，首个面向 Stack Overflow 不完整智能合约代码片段的漏洞检测工具，结合微调 Llama2 补全与符号执行。
面向 Sigmoid 类神经网络鲁棒性验证的可证明最紧线性近似
提出网络级紧致性统一定义，并设计两种可证明最紧的线性近似，显著提升 Sigmoid 类网络鲁棒性验证精度。
神经网络全局鲁棒性的验证
提出面向分类器的全局鲁棒性性质与 anytime 验证器 VHAGaR，计算最小全局鲁棒界并显著优于已有验证器。
发现 ML 系统中的重复代码变更
将 Java 静态分析工具迁移到 Python，挖掘 ML 系统中的重复代码变更模式并开展开发者调研。
面向软件验证算法选择的注意力与表示
提出 Attend and Represent，用注意力与表示学习改进软件验证算法选择，并关注可解释性。
论证明的自然性
用语言模型分析 Coq 与 HOL Light 证明语料，发现证明具有高度可预测的语言规律性，补全可节省超 60% 输入。
BitsAI-CR：基于 LLM 的自动化代码审查实践
提出两阶段 LLM 代码审查框架 BitsAI-CR，以 RuleChecker 检测、ReviewFilter 校验，并在字节跳动大规模落地。
RustAssistant：使用LLM修复Rust代码中的编译错误
用提示技术与LLM-编译器迭代自动修复Rust编译错误，峰值准确率约74%。
基于 GNN 的作业调度器的可扩展验证
提出 vegas，首个可扩展验证基于 GNN 的作业调度器单步与多步性质的形式化框架。
FreshBrew：评估 AI Agent 进行 Java 代码迁移的基准
提出 FreshBrew 基准，系统评估 AI agent 在项目级 Java 迁移中保持语义、避免 reward hacking 的能力。
模型即代码：面向预训练模型枢纽的恶意代码投毒攻击测量研究
首个针对 Hugging Face 预训练模型枢纽恶意代码投毒的系统性测量研究，并提出并落地了检测流水线 MalHug。
面向精度调优的混合精度程序性能与精度预测
用图神经网络学习混合精度程序表示来预测其性能与精度，从而加速动态精度调优。
AI 编程工具的工程陷阱：Claude Code、Codex 与 Gemini CLI 中 bug 的实证研究
首个针对 AI 编程工具的大规模 bug 实证研究，基于 3.8K+ GitHub 报告刻画其失败模式与工程挑战。
通过贝叶斯优化学习实现自适应静态分析
提出用贝叶斯优化从代码库学习参数化分析策略，实现按需流/上下文敏感的自适应静态分析。
Watson：面向 LLM 智能体推理的认知可观测性框架
提出认知可观测性概念与 Watson 框架，用提示归因回溯推断 LLM 智能体的推理轨迹，以支持调试与纠正。
ROCODE：将回溯机制与程序分析集成到大型语言模型中以用于代码生成
提出 Rocode，将程序分析增量检错与回溯重生成融入 LLM 代码生成，提前消除错误并提升通过率、降低开销。
基于语义的神经网络修复
提出基于深度学习层可执行语义的自动修复方法，递归搜索全局最小修改以修复错误神经网络。
CodeLLM-Devkit：一个利用程序分析洞察为代码大模型提供上下文的框架
提出 CodeLLM-Devkit，统一集成多语言静态分析工具，为代码大模型自动提炼程序分析上下文。
VALAR：以值流辅助的主动学习精简静态分析中的告警排序
提出 Valar，用值流分析与主动学习对静态分析告警排序，提升真告警优先级并抑制误报。
通过网络证伪发现属性违反：来自 OpenPilot 的挑战、适配与经验教训
将先进证伪器用于 OpenPilot 的 DNN，揭示真实自动驾驶网络证伪的挑战、工程适配与经验。
面向少像素攻击的深度学习鲁棒性验证
提出 Calzone，首个对 L0（少像素）对抗攻击给出可靠且完备分析的神经网络鲁棒性验证器。
TestWeaver：执行感知、反馈驱动的大语言模型回归测试生成
结合轻量程序分析与 LLM，通过后向切片、相似测试用例和执行内联标注生成回归测试，缓解覆盖率停滞。
学习加速析取式静态缺陷查找器
从数据中学习状态选择启发式，并为每个目标程序自适应挑选最佳模型，显著提升析取式静态缺陷查找效率。
ProofCoop：协作式自动形式化验证
提出 ProofCoop，让多个证明合成模型在搜索中协作，显著提升 Coq 定理自动证明成功率。
Argus：基于分层引用关系的多智能体敏感信息泄露检测框架
提出多智能体框架 Argus，通过分层引用关系检测代码仓库敏感信息泄露并降低误报。
B4：面向似真代码解与似真测试的最优评估
提出贝叶斯框架下用似真测试选择最佳代码解的最优策略及其可计算近似 B4。
具有可证明保证的深度学习安全性与鲁棒性
提出面向深度神经网络的自动验证与测试技术，对有界输入扰动给出可达输出集的上下界，并提供可证明保证。
注意抽象鸿沟：将等价饱和引入真实世界的 ML 编译器
将等价饱和用于真实 ML 计算图，结合全局代价模型优化 XLA，在 CPU/GPU 上平均提速 3.45%。
RACE-Bench：面向仓库级代码智能体特性添加任务的推理增强基准
提出 RACE-Bench，用可执行补丁验证与结构化中间推理轨迹双重评估仓库级代码智能体的特性添加能力。
Prophecy：从神经元激活推断形式化性质
提出工具 Prophecy，通过神经元激活状态自动推断神经网络的形式化性质，支持解释、验证与监控。
一个签名，多次支付：智能合约中签名重放漏洞的揭示与检测
首次实证研究智能合约签名重放漏洞，并提出 LLM 辅助静态污点分析结合符号执行的检测工具 LASiR。
SAINT：结合程序分析与LLM智能体的服务级集成测试生成
提出SAINT，用静态分析构建端点模型与操作依赖图，并借助LLM智能体自动生成企业Java服务级测试。
我们解决智能合约中的访问控制漏洞检测了吗？一项基准研究
构建180个真实访问控制漏洞基准，系统评测SOTA工具与LLM，揭示检测盲区并倡导混合方法。
COBOL 到 Java 转换的自动化测试
提出基于符号执行的测试框架，自动验证 LLM 翻译所得 Java 代码与原始 COBOL 的功能等价性。
面向数据科学代码的知识增强程序修复
提出DSrepair，用知识图谱RAG增强LLM修复数据科学代码缺陷，显著提升修复率并减少token消耗。
协作实现仓库级漏洞检测
通过多智能体协作，将基于 LLM 的漏洞检测从函数级扩展到仓库级，应对跨文件的过程间漏洞。
面向自适应数据分析的程序分析
将自适应性形式化为程序量化性质，并用加权依赖图分析近似其上界，以辅助选择泛化误差控制技术。
EMERGE：通过规则合成检查 LLM 的实现等价性
提出 EMERGE，借助规则合成检查 LLM 的实现等价性，并发布 ASE 2026 工件。
INTENTFIX：通过 LLM 驱动的意图建模实现逻辑漏洞自动修复
提出 INTENTFIX，用 LLM 将开发者意图形式化为模型，差分定位语义缺口并自动合成补丁修复逻辑漏洞。
通过块级依赖分析优化深度学习推理效率
提出 BlockDepend，用块级依赖分析简化算子间依赖并挖掘并行机会，显著加速 DNN 推理。
Meta 的即时捕捉测试生成
提出即时捕捉测试生成，利用代码变更感知与 LLM 筛选生成会失败的测试，在合入前暴露缺陷并降低误报审查负担。
LLM 智能体工作流编排框架中的缺陷特征研究
首个针对 LLM 智能体框架缺陷的大规模实证研究，给出九类根因与六类症状的分类体系。
揭示大语言模型在依据自然语言规约验证代码时的系统性失败
发现并分析 LLM 判断代码是否满足自然语言规约时存在系统性误判，并提出缓解提示策略。