CoVeriTeam: On-Demand Composition of Cooperative Verification Systems

Beyer, Dirk und Kanav, Sudeep (2022): CoVeriTeam: On-Demand Composition of Cooperative Verification Systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2-7, 2022. Fisman, Dana (Hrsg.): In: Tools and algorithms for the construction and analysis of systems. Part 1. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022 : proceedings, Lecture Notes in Computer Science Bd. 13243 Cham, Switzerland: Springer. S. 561-579

Abstract

There is no silver bullet for software verification: Different techniques have different strengths. Thus, it is imperative to combine the strengths of verification tools via combinations and cooperation. CoVeriTeam is a language and tool for on-demand composition of cooperative approaches. It provides a systematic and modular way to combine existing tools (without changing them) in order to leverage their full potential. The idea of cooperative verification is that different tools help each other to achieve the goal of correctly solving verification tasks.

The language is based on verification artifacts (programs, specifications, witnesses) as basic objects and verification actors (verifiers, validators, testers) as basic operations. We define composition operators that make it possible to easily describe new compositions. Verification artifacts are the interface between the different verification actors. CoVeriTeam consists of a language for composition of verification actors, and its interpreter.

As a result of viewing tools as components, we can now create powerful verification engines that are beyond the possibilities of single tools, avoiding to develop certain components repeatedly. We illustrate the abilities of CoVeriTeam on a few case studies. We expect that CoVeriTeam will help verification researchers and practitioners to easily experiment with new tools, and assist them in rapid prototyping of tool combinations.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0302-9743
• Ort: Cham, Switzerland
• Sprache: Englisch