Understanding Counterexamples for Relational Properties with DIbugger
Herda, Mihai 1; Kirsten, Michael
1; Brunner, Etienne 1; Plewnia, Joana 1; Scheler, Ulla 1; Staudenmaier, Chiara 1; Wagner, Benedikt 1; Zwick, Pascal 1; Beckert, Bernhard
1
1 Karlsruher Institut für Technologie (KIT)
1; Brunner, Etienne 1; Plewnia, Joana 1; Scheler, Ulla 1; Staudenmaier, Chiara 1; Wagner, Benedikt 1; Zwick, Pascal 1; Beckert, Bernhard
11 Karlsruher Institut für Technologie (KIT)
Abstract (englisch):
Software verification is a tedious process that involves the analysis of multiple failed verification
attempts, and adjustments of the program or specification. This is especially the case for complex
requirements, e.g., regarding security or fairness, when one needs to compare multiple related runs
of the same software. Verification tools often provide counterexamples consisting of program inputs
when a proof attempt fails, however it is often not clear why the reported counterexample leads to
a violation of the checked property. In this paper, we enhance this aspect of the software
verification process by providing \emph{DIbugger}, a tool for analyzing counterexamples of relational
properties, allowing the user to debug multiple related programs simultaneously.
attempts, and adjustments of the program or specification. This is especially the case for complex
requirements, e.g., regarding security or fairness, when one needs to compare multiple related runs
of the same software. Verification tools often provide counterexamples consisting of program inputs
when a proof attempt fails, however it is often not clear why the reported counterexample leads to
a violation of the checked property. In this paper, we enhance this aspect of the software
verification process by providing \emph{DIbugger}, a tool for analyzing counterexamples of relational
properties, allowing the user to debug multiple related programs simultaneously.
| Zugehörige Institution(en) am KIT | Institut für Theoretische Informatik (ITI) Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL) |
| Publikationstyp | Proceedingsbeitrag |
| Publikationsjahr | 2019 |
| Sprache | Englisch |
| Identifikator | ISSN: 2075-2180 KITopen-ID: 1000096433 |
| Erschienen in | Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (EPTCS), Prague, Czech Republic, 6-7th April 2019. Ed.: E. De Angelis |
| Verlag | Open Publishing Association |
| Seiten | 6–13 |
| Serie | Electronic proceedings in theoretical computer science : EPTCS ; 296 |
| Schlagwörter | Relational properties, Software verification, Debugging |
| Nachgewiesen in | Dimensions Scopus |