# 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.},
place     = {Prague, Czech Republic},
date      = {April 6-7}
}