Publications in Scientific Journals:

A. Bauer, M. Leucker, C. Schallhart, M. Tautschnig:
"Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers";
International Journal on Software Tools for Technology Transfer, 12 (2010), 1; 23 - 37.

English abstract:
This paper describes a method for combining "off-the-shelf" SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning donīt care to as many variables as possible. We then use the generalised solution to determine a thereby smaller constraint set to be handed over to the constraint solver for a background theory. We show that for many benchmarks and real-world problems, this optimisation results in considerably smaller and less complex constraint problems. The presented approach is particularly useful for assembling a practically viable SMT solver quickly, when neither a suitable SMT solver nor a corresponding incremental theory solver is available. We have implemented our approach in the ABsolver framework and applied the resulting solver successfully to an industrial case-study: the verification problems arising in verifying an electronic car steering control system impose non-linear arithmetic constraints, which do not fall into the domain of any other available solver.

SMT - Verification - Constraint solver

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

Created from the Publication Database of the Vienna University of Technology.