
Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Peter van Rossum; Stephan Schulz; Roberto Sebastiani,
Mathsat: Tight Integration of SAT and Mathematical Decision Procedures,
in «JOURNAL OF AUTOMATED REASONING»,
vol. 35,
n. 13,
2005
, pp. 265 
293

C. Curino; M. Giani; M. Giorgetta; A. Giusti; A.L. Murphy; G.P. Picco,
Mobile Data Collection in Sensor Networks: The TinyLime Middleware,
in «PERVASIVE AND MOBILE COMPUTING»,
vol. 1,
n. 4,
2005
, pp. 446 
446

M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; Rossum Peter van; S. P. Schulz; R. Sebastiani,
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic,
Proceedings of 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer,
vol.3440,
2005
, pp. 317
333
, (TACAS 2005,
Edinburgh, UK,
04/04/2005  08/04/2005)

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Peter Schulz; Roberto Sebastiani,
The Mathsat3 System,
Proceedings of 20th Int. Conference on Automated Deduction,
Springer,
vol.3632,
2005
, pp. 315
321
, (CADE20,
Tallin, Estonia,
2227/07/2005)

Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,
Verifying Industrial Hybrid Systems with MathSAT,
Proceedings of 2nd Int. Workshop on Bounded Model Checking,
Elsevier B.V.,
vol.119, issue 2,
2005
, pp. 17
32
, (BMC 2004,
Boston, MA, USA,
18/07/2004)

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,
Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
Proceeding of 17th Int. Conference on Computer Aided Verification,
Springer,
vol.3576,
2005
, pp. 335
349
, (CAV,
University of Edinburgh, Scotland, UK,
610/07/2005)

Roberto Sebastiani; Stefano Tonetta; Moshe Vardi,
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking,
In proc. of the 17th Int. Conference on ComputerAided Verification,
Berlin, Heidelberg,
SpringerVerlag,
vol.3576,
2005
, pp. 100
246
, (CAV 2005,
Edinburgh, Scotland,
610/07/2005)

C. Curino; M. Giani; M. Giorgetta; A. Giusti; A.L. Murphy; G.P. Picco,
TinyLime: Bridging Mobile and Sensor Networks through Middleware,
Washington, DC, USA,
IEEE Computer Society,
2005
, pp. 61
72
, (IEEE International Conference on Pervasive Computing and Communications,
Kauai, Hawaii, USA,
March)

Marco Roveri; Alessandro Cimatti; Andrei Tchaltsev; Roberto Cavada; Simone Semprini; Roderick Bloem; Ingo Pill,
2005,

M. Bozzano; R. Bruttomesso; A. Cimatti; T. Antero Junttila; S. Ranise; Rossum Peter van; R. Sebastiani,
Efficient Theory Combination via Boolean Search,
Many approaches to the decision of quantifier free formulae with respect to a background theory T  also known as Satisfiability Modulo Theory, or SMT(T)  rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory is the combination T1 U T2 of two simpler theories, the approach is typically instantiated by means of a combination schema (e.g. NelsonOppen, Shostak).
In this paper we propose a new approach to SMT(T1 U T2), where the enumerator of truth assignments is integrated with two decision procedures for T1 and for T2, which act independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the purified formula, but also to all the equalities between interface variables.
This approach is simple and expressive: for instance, no modification is required to handle nonconvex theories (as opposed to traditional NelsonOppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on stateoftheart boolean and SMT search techniques, and on theory layering (i.e. cheaper reasoning first, and more often).
We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (EUF) and Linear Arithmetic (LA), both for (the convex case of) reals and for (the nonconvex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with competitor tools, obtaining speedups up to two orders of magnitude,
2005