  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.
