论文标题
通过集体不变一代的合作验证
Cooperative Verification via Collective Invariant Generation
论文作者
论文摘要
由于开发了新的验证方法以及诸如SMT解决方案之类的支持技术，软件验证最近已取得了巨大进展。为了使软件验证工具与这些进步保持最新状态，工具开发人员几乎完全通过在自己的框架内重新实现该方法来将新设计的方法集成到其工具中。尽管这允许重新使用方法，但它需要为每种新技术进行新颖的实现。 在本文中，我们采用合作验证，以避免重新实现并使新工具用作验证中的黑盒组件。具体而言，合作用于软件验证的核心成分，这是不变生成的。找到足够的循环不变是验证运行成功的关键。我们名为CoverCig的框架允许使用主验证工具将不变生成的任务委托给一个或几个专用的助手不变发电机。然后在主验证者的验证运行中使用它们的结果，尤其允许交叉检查不变性的有效性。我们通过使用SV-Comp 2020的许多基准测试了两个大师和三个不同不变的发电机的实验评估我们的框架。实验表明，Covercig的使用可以增加正确验证的任务的数量而无需增加所用资源
Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid reimplementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVerCIG allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVerCIG can increase the number of correctly verified tasks without increasing the used resources
