LLM 结合代码属性图可为 C 代码合成 ACSL 帧规范，作者报告成功率 92.9%。
资讯摘要
论文提出 AutoFraming，一种基于 LLM 从 C 代码合成 ACSL 帧规范（frame conditions）的方法，弥补现有工作偏重功能契约与循环不变式、忽视帧条件的不足。方法通过分析代码属性图（CPG）提取与帧相关的信息来引导 LLM 生成帧条件，覆盖区域分离约束与数据依赖。作者报告在 84 个真实系统函数的基准上，92.9% 的函数可生成无错误帧规范，相对当前最优方法提升 179%；另一 51 函数基准上成功率从 80.4% 升至 96.1%。
要点速读
- 方法用代码属性图（CPG）提取帧相关信息，引导 LLM 生成 ACSL 帧规范，同时覆盖区域分离约束与数据依赖。
- 在 84 个来自真实系统的 ACSL 兼容函数上，92.9% 生成无错误帧规范，作者称相对当前最优方法提升 179%。
- 在 51 个函数的第二个基准上成功率由 80.4% 升至 96.1%；作为辅助组件接入现有 LLM 合成框架可提升帧规范生成最多 61.9%。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/23 08:00:11（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。