Understanding Counterexamples for Relational Properties with DIbugger
Authors:
Mihai Herda,
Michael Kirsten,
Etienne Brunner,
Joana Plewnia,
Ulla Scheler,
Chiara Staudenmaier,
Benedikt Wagner,
Pascal Zwick,
Bernhard Beckert
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…
▽ More
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.
△ Less
Submitted 9 July, 2019;
originally announced July 2019.
Reducing the Complexity of Quantified Formulas via Variable Elimination
Authors:
Aboubakr Achraf El Ghazi,
Mattias Ulbrich,
Mana Taghdiri,
Mihai Herda
Abstract:
We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite s…
▽ More
We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite set of sufficient ground terms can be eliminated by instantiating them with the computed ground terms. The resulting SMT formula contains potentially fewer quantifiers and thus is potentially easier to solve. We describe how a satisfying model of the resulting formula can be modified to satisfy the original formula. Our experiments show that in many cases, this simplification considerably improves the solving time, and our evaluations using Z3 and CVC4 indicate that the idea is not specific to a particular solver, but can be applied in general.
△ Less
Submitted 4 August, 2014;
originally announced August 2014.
