使用CIVL验证PETSc：基于LLM生成的ACSL契约与确定性驱动程序生成
Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
浏览论文内容
中文总结 AI 辅助
本文提出利用LLM生成ACSL契约和确定性驱动程序，结合CIVL验证器，对PETSc数值库函数进行形式验证，并成功发现MatAYPX中自1997年存在的未发现错误。
中文摘要 AI 辅助
并行数值库（如PETSc）广泛应用于科学与工程应用中，在这些应用中，错误结果可能带来高昂的代价。尽管如此，数值库很少经过正式验证。挑战之一在于需要专家手动编写规范并手动应用验证工具，这通常需要开发测试平台或驱动程序，而所有这些都可能包含额外的错误，导致验证过程中出现误报或漏报。随着大型语言模型（LLM）的最新进展，自动生成此类驱动程序和参考模型颇具吸引力，但基于简单提示的一次性生成是脆弱的，并会导致需要审计的额外未验证代码。在本文中，我们提出了一种方法，在有限设置下使用LLM，根据函数文档生成一个小型、可人工认证的ACSL契约，并结合一个支持受限ACSL配置文件的确定性工具链，生成一个使用CIVL验证器来检查实现是否符合契约的驱动程序，并在可用时使用现有的参考模型。我们在三个PETSc函数上端到端地演示了该流水线：MatAXPY（参考模型已存在）、MatAYPX（无参考模型，因此认证契约是唯一标准）以及MatFilter的非压缩模式（无参考模型，具有更复杂的条件行为）。通过该流水线，我们能够发现PETSc中MatAYPX函数的一个此前未被发现的错误，该错误自1997年以来一直存在于代码中。
英文摘要
Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical libraries are rarely formally verified. One of the challenges is the need for an expert to hand-write a specification and manually apply a verification tool, often requiring the development of a harness or driver, all of which can contain additional bugs that lead to false positives or false negatives during verification. With recent advancements in large language models (LLMs), it is tempting to generate such drivers and reference models automatically, but one-shot generation based on a simple prompt is brittle and leads to additional unverified code that needs to be audited. In this paper, we present an approach to use LLMs in a limited setting to generate a small, human-certifiable ACSL contract from the function's documentation, combined with a deterministic toolchain that supports a restricted ACSL profile and generates a driver that uses the CIVL verifier to check the implementation against the contract and, when available, an existing reference model. We demonstrate the pipeline end-to-end on three PETSc functions: MatAXPY (reference model already exists), MatAYPX (no reference model, so the certified contract is the sole oracle), and the non-compressing mode of MatFilter (no reference model, with more complex, conditional behavior). With this pipeline, we were able to discover a bug in PETSc's MatAYPX function that was previously undiscovered and had been present in the code since 1997.
