[Zurück]


Zeitschriftenartikel:

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; S. 23 - 37.



Kurzfassung englisch:
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.

Schlagworte:
SMT - Verification - Constraint solver


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/s10009-009-0133-2


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.