Understanding Counterexamples for Relational Properties with DIbugger

Reviewed Paper In Proceedings

Author(s):Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard Beckert
In:Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019)
Publisher:Open Publishing Association
Series:EPTCS
Volume:296
Year:2019
Pages:6-13
DOI:10.4204/EPTCS.296.4

Abstract

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 DIbugger, a tool for analyzing counterexamples of relational properties, allowing the user to debug multiple related programs simultaneously.

BibTeX

@InProceedings{HerdaKirstenEA2019,
  author    = {Mihai Herda and
               Michael Kirsten and
               Etienne Brunner and
               Joana Plewnia and
               Ulla Scheler and
               Chiara Staudenmaier and
               Benedikt Wagner and
               Pascal Zwick and
               Bernhard Beckert},
  title     = {Understanding Counterexamples for Relational Properties with DIbugger},
  booktitle = {Sixth Workshop on Horn Clauses for Verification and Synthesis and
               Third Workshop on Program Equivalence and Relational Reasoning ({HCVS}/{PERR} 2019)},
  editor    = {Emanuele De Angelis and
               Grigory Fedyukovich and
               Nikos Tzevelekos and
               Mattias Ulbrich},
  series    = {EPTCS},
  volume    = {296},
  publisher = {Open Publishing Association},
  pages     = {6-13},
  doi       = {10.4204/EPTCS.296.4},
  month     = jul,
  year      = {2019},
  abstract  = {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.},
  venue     = {Prague, Czech Republic},
  eventdate = {2019-04-06/2019-04-07}
}