代码大模型 / AI 编程

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

生成式编译：人工智能生成代码时的即时编译器反馈

Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, Jingxuan He

机构 * ETH Zurich（苏黎世联邦理工学院） ； Sofia University ``St. Kliment Ohridski''（索菲亚大学） ； University of California, Berkeley（加州大学伯克利分校） 纠错

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.AI、cs.LG、cs.PL

AI总结 研究针对人工智能生成代码时的问题，提出生成式编译方法，核心是sealor技术，能在生成中获取编译器反馈，在Rust编码任务中评估，减少非编译输出、提高功能正确性，使编译器在生成阶段发挥更重要作用。

FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification

FVRuleLearner：基于操作级推理树（OP-Tree）的规则学习用于形式验证

Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai, Cunxi Yu, Ghaith Bany Hamad, Deming Chen, Haoxing Ren

机构 * University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； NVIDIA（英伟达） ； University of Maryland, College Park（马里兰大学帕克分校） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.SE、cs.AI

AI总结 本文提出FVRuleLearner，通过操作级推理树模型，提升形式验证中SVA操作符选择的准确性和效率，显著提高语法和功能正确性。

Comments Accepted to IEEE VTS'26

ATLAS: Multi-View Code Representation Tool for C and C++ Source Programs

ATLAS: C和C++源代码的多视图代码表示工具

Jaid Monwar Chowdhury, Ahmad Farhan Shahriar Chowdhury, Humayra Binte Monwar, Mahmuda Naznin

专题命中 程序分析与验证 ：repository(abstract,comments)；分类 cs.SE

AI总结 提出ATLAS工具，无需完整构建即可为C/C++生成对齐的AST、CFG和DFG，支持部分输入，输出JSON/DOT/PNG，在TheAlgorithms语料上CFG正确率达96.80%（C）和91.67%（C++）。

Comments 5 pages, 4 figures, 2 tables; Video demonstration: https://youtu.be/50DvEbenp14; Tool repository: https://github.com/jaid-monwar/ATLAS-multi-view-code-representation-tool.git

Source-Free Detection and Impact Analysis of Compiler Optimization Problems in Mobile Applications

移动应用中编译器优化问题的无源检测与影响分析

Han Hu, Xiaoheng Xie, Bo Sun, Jian Gu, Gang Fan, Li Li

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE

AI总结 提出无源框架OptDetect，直接从二进制文件检测编译器优化问题，无需源码或构建元数据，准确率达93.0%，发现30.5%的库使用低优化级别，修复后CPU指令减少10-63%。

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

KVerus：面向Rust代码的可扩展且高鲁棒性的形式化验证证明生成工具

Yuwei Liu, Xinyi Wan, Yanhao Wang, Minghua Wang, Lin Huang, Tao Wei

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE

AI总结 KVerus是适配Rust代码的形式化验证工具，通过自适应范式与动态知识库，在单文件、仓库级基准及Rust内核验证中均优于现有方案，为形式化验证的规模化应用提供了关键进展。

Comments Accepted at ASE 2026