一句话：提出 Preguss，以潜在运行时错误引导静态分析与 LLM 分治合成过程间规约，实现千行级程序的高自动验证。
大规模软硬件系统的全自动验证是形式方法的终极目标之一。LLM 虽可提升演绎验证中形式规约生成的自动化程度，但受长上下文推理限制，且难以推断复杂的过程间规约，因而可扩展性差。本文提出 Preguss——一个模块化、细粒度的形式规约自动生成与精化框架。Preguss 以分治方式协同静态分析与演绎验证：一方面基于潜在运行时错误（RTE）构建并优先排序验证单元，另一方面在单元级别借助 LLM 合成过程间规约。实验表明，Preguss 显著优于当前最先进的基于 LLM 的方法，能够对超过一千行代码的真实程序实现高度自动的 RTE-free 验证，并将人工验证工作量减少 80.6%~88.9%。
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to long-context reasoning limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper presents Preguss – a modular, finegrained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by steering two components in a divide-and-conquer fashion: (i) potential runtime error-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We show that Preguss substantially outperforms state-of-the-art LLM-based approaches and, in particular, it enables highly automated RTE-freeness verification for real-world programs with over a thousand LoC, with a reduction of 80.6%~88.9% human verification effort.
@article{paperbot3835,
title = {A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs},
author = {Zhongyi Wang and Tengjie Lin and Mingshuai Chen and Haokun Li and Mingqi Yang and Xiao Yi and Shengchao Qin and Yixing Luo and Xiaofeng Li and Bin Gu and Liqiang Lu and Jianwei Yin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798268}
}