Skip navigation
Skip navigation

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

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

Description

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
URI: http://hdl.handle.net/1885/57004
Source: International Journal on Software Tools for Technology Transfer
DOI: 10.1007/s10009-009-0133-2

Download

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:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator