Skip navigation
Skip navigation
The system will be down for maintenance between 8:00 and 8:15am on Thursday 13, December 2018

Don't care in SMT: Building flexible yet efficient abstraction/refinement solvers

Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael


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...[Show more]

CollectionsANU Research Publications
Date published: 2010
Type: Journal article
Source: International Journal on Software Tools for Technology Transfer
DOI: 10.1007/s10009-009-0133-2


File Description SizeFormat Image
01_Bauer_Don't_care_in_SMT:_Building_2010.pdf706.85 kBAdobe PDF    Request a copy
02_Bauer_Don't_care_in_SMT:_Building_2010.pdf183.49 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  27 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator