Understanding Counterexamples for Relational Properties with DIbugger

@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}
}