ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification

📄 arXiv: 2605.27051v1 📥 PDF

作者: Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous, Konstantin Korovin, Lucas C. Cordeiro

分类: cs.SE, cs.AI

发布日期: 2026-05-26

备注: 12 pages; 6 figures

💡 一句话要点

ConVer：利用合约与循环不变式综合实现可扩展的形式化软件验证

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 软件验证 大型语言模型 合约综合 CEGAR-CEGIS

📋 核心要点

  1. 现有C程序形式化验证方法面临状态空间爆炸问题，难以处理大型程序。
  2. ConVer利用LLM综合函数合约，并通过CEGAR-CEGIS循环进行系统级和函数级验证，实现自顶向下的组合验证。
  3. 实验表明，ConVer在多个基准测试中取得了优于现有工具的验证成功率，尤其是在简单C程序和LF-Hard基准上。

📝 摘要（中文）

大型C程序的形式化验证面临状态空间爆炸问题：有界模型检查(BMC)工具必须通过展开所有嵌套结构来编码达到预定界限的整个状态空间。本文提出ConVer，一种自顶向下的组合验证工具。给定一个带有顶层断言的C程序，ConVer自顶向下地分解验证：它使用大型语言模型(LLM)从系统属性中综合函数合约，然后在CEGAR-CEGIS循环中交替进行系统级和函数级检查，并通过SMART ICE学习在检查失败时细化合约。我们在四个难度递增的基准测试套件上评估ConVer，并与其他最先进的(SOTA)工具进行比较。在包含45个简单C程序的Frama-C基准测试中，ConVer在三个LLM后端上实现了82-96%的验证成功率，其中93-95%的收敛程序仅需要一次CEGAR-CEGIS迭代。在X.509解析器基准测试(6个程序)和LF2C-Simple套件(17个程序)上，ConVer分别实现了33-50%和82-88%的成功率。在包含11个递归和循环密集型程序的VerifyThis套件上，Pre-Abstraction策略实现了55-64%的成功率。此外，我们还提出了ESBMC-LF，一个预处理器工具，可以将LF模型转换为C，同时保留LF文件的属性，使ConVer能够验证它们。我们使用ESBMC-LF将LF Verifier Benchmarks转译为C；我们将其表示为LF-Hard。我们表明ConVer成功验证了总体67%的LF-Hard基准。

🔬 方法详解

问题定义：大型C程序的形式化验证由于状态空间爆炸而面临挑战。传统的有界模型检查(BMC)方法需要展开所有嵌套结构，导致计算复杂度极高，难以处理复杂程序。现有方法在处理包含大量循环和递归的程序时，验证效率和可扩展性都存在瓶颈。

核心思路：ConVer的核心思路是采用自顶向下的组合验证方法，将复杂的验证任务分解为更小的、可管理的子任务。通过使用大型语言模型(LLM)自动生成函数合约，并利用CEGAR-CEGIS循环迭代地细化这些合约，从而降低了验证的复杂性。这种方法允许在系统级别和函数级别之间进行交替检查，有效地控制了状态空间的大小。

技术框架：ConVer的整体框架包含以下几个主要模块：1) LLM合约综合器：使用LLM从系统属性中自动生成函数合约。2) CEGAR-CEGIS循环：在系统级别和函数级别之间交替进行验证检查。如果检查失败，则通过SMART ICE学习细化合约。3) ESBMC-LF预处理器：将LF模型转换为C代码，以便ConVer可以验证LF基准。整个流程从顶层断言开始，逐步分解验证任务，直到所有子任务都被验证通过。

关键创新：ConVer的关键创新在于将大型语言模型(LLM)引入到形式化验证流程中，用于自动生成函数合约。这极大地减少了人工干预的需求，并提高了验证的效率。此外，ConVer采用的CEGAR-CEGIS循环和SMART ICE学习策略能够有效地细化合约，从而提高验证的准确性和可靠性。

关键设计：ConVer的关键设计包括：1) LLM的选择和训练：选择合适的LLM，并使用相关的代码和规范数据进行训练，以提高合约生成的质量。2) CEGAR-CEGIS循环的迭代策略：设计有效的迭代策略，以确保合约能够快速收敛到正确的状态。3) SMART ICE学习算法：使用SMART ICE学习算法来细化合约，从而提高验证的准确性。4) ESBMC-LF预处理器的实现：确保LF模型转换为C代码时，能够保留原始模型的属性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

ConVer在Frama-C基准测试中取得了82-96%的验证成功率，在X.509解析器和LF2C-Simple套件上分别达到了33-50%和82-88%的成功率。在VerifyThis套件上，Pre-Abstraction策略实现了55-64%的成功率。此外，ConVer成功验证了67%的LF-Hard基准，表明其在处理复杂程序验证方面的有效性。

🎯 应用场景

ConVer可应用于各种安全关键型软件系统的形式化验证，例如操作系统内核、嵌入式系统、网络协议和加密算法等。通过自动生成函数合约和迭代细化验证，ConVer能够有效地检测软件中的潜在错误和漏洞，提高软件的可靠性和安全性，并降低开发和维护成本。该研究对于提升软件质量和保障信息安全具有重要意义。

📄 摘要（原文）

Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a top-down compositional verification tool. Given a C program with a top-level assertion, ConVer decomposes verification top-down: it uses a large language model (LLM) to synthesise function contracts from the system property, then alternates system-level and function-level checks in a CEGAR-CEGIS loop, refining contracts whenever a check fails via SMART ICE learning. We evaluate ConVer on four benchmark suites of increasing difficulty and against other state-of-the-art (SOTA) tools. On the Frama-C benchmark of 45 simple C programs, ConVer achieves 82-96% verification success across three LLM backends, with 93-95% of converged programs requiring only a single CEGAR-CEGIS iteration. On the X.509 parser benchmark (6~programs) and LF2C-Simple suite (17 programs), ConVer achieves 33-50% and 82-88% success respectively. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55-64% success. In addition, we present ESBMC-LF a preprocessor tool that converts LF models to C while preserving the properties of the LF files, enabling ConVer to verify them. We transpile the LF Verifier Benchmarks using ESBMC-LF to C; we denote those LF-Hard. We show that ConVer successfully verifies 67% of LF-Hard benchmarks overall.