一句话：用LLM生成循环不变式并由一阶定理证明器校验，从而在CFG层面消除循环，扩展有界模型检测对无界循环程序的验证能力。
经典有界模型检测（BMC）通常通过循环展开来处理程序中的循环，这限制了对无界循环程序的验证能力。本文研究一种改进的BMC流程：不再展开循环，而是修改控制流图（CFG），将表示循环的CFG片段替换为一个断言该循环不变式的节点。作者利用大语言模型（LLM）生成这些循环不变式，并使用一阶定理证明器验证所生成断言语句的正确性，从而以可靠（sound）的方式将程序转化为无循环变体。基于该方法的工具ESBMC ibmc在实验评估中表现出与当前最先进形式验证器相当的竞争力，显著提升了工业级软件验证器ESBMC可验证的程序数量，并成功验证了SeaHorn和VeriAbs等先进验证器无法验证的一些程序。
We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node asserting invariants of the loop. We generate these invariants using Large Language Models (LLMs) and use a first-order theorem prover to ensure the correctness of the generated statements. We thus transform programs to loop-free variants in a sound manner. Our experimental results show that the resulting tool, ESBMC ibmc, is competitive with state-of-the-art formal verifiers for programs with unbounded loops, significantly improving the number of programs verified by the industrial-strength software verifier ESBMC and verifying programs that state-of-the-art software verifiers such as SeaHorn and VeriAbs could not.
@inproceedings{PirzadaRBC24,
title = {LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling},
author = {Muhammad A. A. Pirzada and Giles Reger and Ahmed Bhayat and Lucas C. Cordeiro},
booktitle = {ASE},
year = {2024},
doi = {10.1145/3691620.3695512}
}