Exploring cooperative verification

Kanav, Sudeep (2024): Exploring cooperative verification: survey, tools, and experiments. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

No silver bullet exists for software verification: Many successful tools and techniques have been developed over the past few decades, but none of them is sufficient to tackle the problem on its own. Each of these successful tools and techniques is strong in some specific areas but weak in others. With this background, it is natural to try out combinations of verification techniques. These combinations could either be integrated or constructed using off-the-shelf components, where the components may exchange information. This thesis explores the area of cooperative verification. A cooperative verification technique is a combination of verification techniques where different off-the-shelf components work together, as a team, sharing information with each other with the goal of solving a verification problem. As a first step, we reviewed scientific literature to understand and systematize the knowledge about cooperative verification. We found that most of these combinations were developed ad hoc. To address this gap, we developed CoVeriTeam, a tool for systematic construction and execution of combinations of verification tools. We conducted an extensive evaluation of tool combinations constructed using CoVeriTeam to investigate their performance in comparison to the standalone tools when solving verification problems. Furthermore, to improve the accessibility of verification tools, we have developed a web service for CoVeriTeam that allows users to execute verification tools and their combinations remotely. Our work is already having an impact: (1) CoVeriTeam was used in research work to construct an off-the-shelf component-based counterexample-guided abstractionrefinement tool, (2) two tools constructed using CoVeriTeam participated in the 11th Competition on Software Verification held in 2022, (3) CoVeriTeam Service was used in integration scripts for the 2023 competitions on software verification and testing to check if the submitted tools can be successfully executed, and (4) a user interface based on an instance of CoVeriTeam Service has been developed at Huawei Dresden Research Center to demonstrate the capabilities of verification tools and allow other teams at Huawei to use these tools without needing to install them.

Abstract

Es gibt kein Patentrezept für die Softwareverifikation: In den letzten Jahrzehnten wurden viele erfolgreiche Werkzeuge und Techniken entwickelt, jedoch kommen diese mit ihren eigenen Stärken und Schwächen. Für bestimmte Anwendungsbereiche sind einige Techniken und Werkzeuge daher besser geeignet als andere. Deshalb liegt es nahe, verschiedene Kombinationen von bestehenden Verifikationstechniken auszuprobieren. Diese Kombinationen können in bestehende Werkzeuge integriert oder direkt aus bereits verfügbaren Komponenten zusammengesetzt werden. Hierbei tauschen die Komponenten unter Umständen Informationen aus, um schneller ein Ergebnis zu erzielen. Diese Arbeit konzentriert sich auf kooperative Verifikation, also die Kombination von bestehenden Verifikationskomponenten. Dabei arbeiten die Komponenten als Team; sie tauschen Informationen untereinander aus, um gemeinsam das zugrundeliegende Verfikationsproblem zu lösen. Zu Beginn der Arbeit werden bereits existierende kooperative Techniken in einer systematischen Literaturstudie eingeordnet, verstanden und kategorisiert. Das Ergebnis der Studie legt nahe, dass viele kooperative Techniken ad hoc implementiert werden. Basierend auf dieser Erkenntnis, wurde CoVeriTeam entwickelt. Es erlaubt, dass kooperative Ansätze innerhalb eines Frameworks systematisch konstruiert und ausgeführt werden können. Mithilfe von CoVeriTeam können verschiedene Kombinationen von Techniken auch evaluiert werden. Das Ergebnis: Tatsächlich übertrifft die Kombination der Techniken die Leistungen der einzelnen Komponenten. Zudem vereinfacht CoVeriTeam die Nutzung von bestehenden Komponenten durch einen Webservice, welcher es Nutzern erlaubt, eine Vielzahl von Verifikationswerkzeugen und - techniken auszuprobieren – ganz ohne diese installieren zu müssen. Die Ergebnisse dieser Forschungsarbeit werden bereits erfolgreich in wichtigen Bereichen der formalen Verifikation eingesetzt: (1) CoVeriTeam wurde in einer Forschungsarbeit für einen komponentenbasierten Ansatz für das sogenannte Counter-example Guided Abstraction Refinement (CEGAR) eingesetzt, (2) Zwei Werkzeuge, die mit CoVeriTeam erstellt wurden, haben im elften internationalen Wettbewerb für Softwareverifikation 2022 (SV-COMP 2022) teilgenommen, (3) Unser CoVeriTeam Service wurde vor der Ausführung der SV-COMP 2023 benutzt, um teilnehmenden Teams vorab unkompliziert mitzuteilen, ob die eingereichte Software auf der vorhanden Infrastruktur ausgeführt werden kann, (4) Das Huawei Dresden Research Center auf CoVeriTeam aufbauen eine Schnittstelle für Abgestellte bereitgestellt, welche es erlaubt Verifikationswerkzeuge ohne vorherige Installation benutzen können.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Cooperative Verification, Tool Development, Software Verification, Automatic Verification, Verification Tools, Tool Composition, Tool Reuse
• Themengebiete: 000 Allgemeines, Informatik, Informationswissenschaft ; 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 23. April 2024
• 1. Bericht­erstatter:in: Beyer, Dirk