arXiv cs.AI· Han Zhou, Yu Luo, Dianxiang Xu·· 12 小时前AI 评分23
AutoFraming：用 LLM 为 C 代码合成动态 frame 规约
AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs
AI 导读
AutoFraming 提出一种基于 LLM 的方法，从 C 代码中同时合成 ACSL frame 规约与功能契约，通过分析代码属性图（CPG）提取 frame 相关信息来引导 LLM 生成准确的 frame 条件。
正文 · AI 翻译
摘要：大型语言模型（LLM）在从源代码合成形式化规约方面已展现出相当大的潜力。然而，现有方法主要关注功能契约和循环不变式，而在很大程度上忽略了框架条件，框架条件规定了执行期间可能或不可能被修改的内存位置，是形式化规约的重要组成部分。为解决这一局限，我们提出了一种基于 LLM 的方法，用于从 C 代码中合成 ACSL 框架规约以及功能契约。我们的方法分析代码属性图（CPG），从输入代码中提取与框架相关的信息，并利用这些信息引导 LLM 生成准确的框架条件。生成的规约同时捕获了区域分离约束和支配变量修改的数据依赖关系。实验结果证明了我们方法的有效性。在来自非平凡真实系统的 84 个符合 ACSL 的函数基准上，我们的方法成功为 92.9% 的函数合成了无错误的框架规约，相较于最先进技术实现了 179% 的相对提升。在由 51 个函数组成的第二个基准上，成功率从 80.4% 提升至 96.1%。此外，当作为辅助组件集成到现有的基于 LLM 的 ACSL 合成框架中时，我们的方法将框架规约生成性能提升高达 61.9%。
| 评论： | 12 页，1 幅图，6 张表 |
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.29046 [cs.AI] |
| （或 arXiv:2610.29046v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.29046 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Yu Luo [查看邮箱]
[v1]
2026 年 10 月 21 日星期三 01:22:00 UTC（501 KB）
来源：arXiv cs.AI · arxiv.org