智能体驱动的大规模程序规约生成与自动化验证

报告摘要: 本文提出 Preguss，一个结合静态分析、演绎验证与大语言模型的规约自动生成框架。其采用分而治之策略，首先根据证明目标（即潜在运行时错误断言）构建并排序验证单元，然后合成并精化单元级过程间规约，并保证可靠性与终止性。实验表明，Preguss优于现有先进方法，可对千行以上工业程序实现高自动化内存安全验证，将人工验证工作量减少 80.6%–88.9%，并发现了某航天器控制软件中的6个真实运行时错误。

报告人简介: 王钟逸，浙江大学计算机科学与技术学院博士生，导师是陈明帅研究员。主要研究方向是程序自动化验证与静态分析。相关研究成果发表于OOPSLA、ASE、J. Comput. Sci. Technol.等领域重要国际会议/期刊。