Leveraging invariant information towards incremental Software Model Checking

Spiessl, Martin (2024): Leveraging invariant information towards incremental Software Model Checking. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

Automatic Software Model Checking has become more and more powerful over the recent years. While the tools have improved, the means of exchange of information as well as the kind of information that is exchanged, are lacking behind. This is a limiting factor for progress in the field, as a lot of potential lies in the exchange and careful dissemination of computed information. Currently, information about the proof or counterexample can be extracted in the form of witness automata that refer to the program’s control-flow automaton (CFA). These witnesses can then be checked by a validator, which is an important step that increases the trust in the verification result. However, this format suffers from imprecision in its semantics, since the CFA of a program is usually not defined by the language standard. Furthermore, in its current form, the format is syntactically limited to invariants that can be written as expressions in the program’s language. This is in strong contrast to the deductive verification community, where proofs usually require more elaborate syntactical features. Lastly, the way how this information is (re-)used is very limited. Until recently, the only use case was the validation of verification results. In case the validation fails, it is often unclear how to gain insights from that. We improve upon the state of the art in the following ways: Regarding the exchange format, we identify the areas in which the established format is imprecise and evaluate whether we can improve upon this. As solution, we propose an alternative format whose semantics is well-defined. Using this format, we showcase how extensions can be gradually incorporated by automatic software verifiers. With respect to exchanging information between tools, we first show a way how information from the witnesses can be encoded back into a verification problem. As an extension of this, we demonstrate how this approach can be used to construct a deductive verifier from existing, automatic verifiers, using the witnesses as an established interface. This way, verification results can be reused in an incremental fashion more easily or even complemented via user interaction.

Abstract

Automatisches Software-Model-Checking ist in den letzten Jahren immer leistungsfähiger geworden. Während sich die Tools verbessert haben, haben sich die Austauschformate für Informationen sowie die Art der ausgetauschten Informationen nicht in selbem Maße weiterentwickelt. Dies ist ein limitierender Faktor für Fortschritte in diesem Bereich, da gerade jüngste Ansätze zeigen, dass viel Potenzial im Austausch und der Wiederverwendung der berechneten Informationen liegt. Derzeit können Informationen über den Beweise oder Gegenbeispiele in Form von Automaten extrahiert werden, die sich auf den Kontrollflussautomaten (CFA) des Programms beziehen. Diese Zeugen können dann von einem sogenannten Validator überprüft werden, was ein wichtiger Schritt ist, um das Vertrauen in das Verifizierungsergebnis zu erhöhen. Dieses Format leidet jedoch unter einer unvollständigen Spezifikation seiner Semantik, da der CFA eines Programms in der Regel nicht durch den Sprachstandard definiert ist. Des Weiteren ist das Format in seiner derzeitigen Form syntaktisch auf Invarianten beschränkt, die als Ausdrücke in der Sprache des Programms geschrieben werden können. Das steht im starken Kontrast zur Gemeinschaft rund um die deduktiven Verifikation, wo Beweise normalerweise ausführlichere syntaktische Merkmale erfordern. Schließlich ist die Art und Weise, wie diese Informationen wiederverwendet werden, sehr eingeschränkt. Bis vor kurzem war der einzige Anwendungsfall die Validierung von Verifizierungsergebnissen. Falls die Validierung fehlschlägt, ist es oft unklar, wie man daraus Erkenntnisse gewinnen kann. Wir verbessern den Stand der Technik in folgender Weise: Bezüglich des Austauschformats identifizieren wir die Bereiche, in denen das etablierte Format ungenau ist und untersuchen, in welcher Weise diese Ungenauigkeit behoben werden kann. Als Lösung schlagen wir ein alternatives Format vor, dessen Semantik klar definiert ist. Mit diesem Format zeigen wir, wie Erweiterungen schrittweise von automatischen Programmverifizierern integriert werden können. In Bezug auf den Informationsaustausch zwischen den Verifikations-Tools zeigen wir zuerst, wie Informationen aus den Witnesses in ein Verifizierungsproblem zurück kodiert werden können. Als Erweiterung davon zeigen wir, wie dieser Ansatz verwendet werden kann, um einen deduktiven Verifier aus bestehenden automatischen Verifiern zu erstellen, wobei die Witnesses als etablierte Schnittstelle dienen. Auf diese Weise können Verifizierungsergebnisse leichter schrittweise wiederverwendet werden oder sogar durch Benutzerinteraktion ergänzt werden.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Software verification, Program analysis, Loop abstraction, Precision adjustment, Counterexample-guided abstraction refinement
• 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: 22. Mai 2024
• 1. Bericht­erstatter:in: Beyer, Dirk