用LLM生成ACSL规约，并以CIVL验证PETSc函数

PETSc 等并行数值库广泛应用于科学和工程应用中，在这些应用中，错误的结果可能会产生代价高昂的后果。尽管如此，数值库很少得到正式验证。挑战之一是需要专家手写规范并手动应用验证工具，通常需要开发Harness或驱动程序，所有这些都可能包含额外的错误，导致验证期间出现误报或漏报。随着大语言模型 (LLM) 的最新进展，自动生成此类驱动程序和参考模型很诱人，但基于简单提示的一次性生成很脆弱，并且会导致需要审核的额外未经验证的代码。在本文中，我们提出了一种在有限环境中使用 LLM 的方法，从功能文档中生成小型的、可人工认证的 ACSL 合同，并结合支持受限 ACSL 配置文件的确定性工具链，并生成一个驱动程序，该驱动程序使用 CIVL 验证器来检查实现是否符合合同，并在可用时与现有参考模型对照（如果可用）。我们在三个 PETSc 函数上演示了端到端的管道：MatAXPY（参考模型已经存在）、MatAYPX（没有参考模型，因此经过认证的合约是唯一的预言机）和 MatFilter 的非压缩模式（没有参考模型，具有更复杂的条件行为）。通过这个管道，我们能够发现 PETSc 的 MatAYPX 函数中的一个错误，该错误以前未被发现，并且自 1997 年以来一直存在于代码中。