多样化验证：当任务等效程序的可验证性不同时

程序验证对于软件的正确性至关重要，但在实践中生成经过充分验证的程序仍然很困难。本文研究当多个生成的程序旨在满足相同的任务级语义时，实现结构是否会影响自动验证性。我们提出了 Diversify2Verify，这是一个用于 Why3 的​​基于 LLM 的分阶段管道，它推断特定于表示的合约，生成和测试各种递归和命令式数组/列表实现，并尝试使用有界验证者引导的注释修复进行验证。我们还构建了一个针对整数、数组和列表的 73 个任务的面向验证的基准，产生 292 个实现变体。 Diversify2Verify 最初验证了 96 个工件，两次修复后验证了 154 个工件，将工件级别验证从 32.9% 提高到 52.7%。在任务级别，73 项任务中的 49 项至少有一种变体得到验证，成功率为 67.1%。这些结果表明，任务等效实现在可验证性方面可能存在很大差异，并且实现多样性有助于找到易于验证的工件。