Publications
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis.
(Tech. Rep. version available here) -
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani.
To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T).
(Tech. Rep. version available here) -
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Silvio Ranise, Roberto Sebastiani
"Efficient Theory Combination via Boolean Search".
Information and Computation. Elsevier. To appear. -
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
"MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure".
Journal of Automated Reasoning. Kluwer. To appear. -
M. Bozzano, R. Bruttomesso, A. Cimatti, Z. Hanna, A. Palti, Z. Kashidashvili, R. Sebastiani
"Encoding RTL Constructs for MathSAT: a Preliminary Report".
Proc. 3rd Int. workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'05). ENTCS series, Volume 144, issue 2, 2006. Ed. Elsevier. -
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
"The MathSAT 3 System".
In proc. CADE-20, Int. Conference on Automated Deduction, 2005, Tallin, Estonia, July 2005. LNCS, No 3632 Springer. -
M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Ranise, R. Sebastiani
"Efficient Satisfiability Modulo Theories via Delayed Theory Combination".
In proc. Int. Conf. on Computer-Aided Verification, CAV 2005. LNCS, No 3576. Springer. -
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
"An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic".
In proc. TACAS2005, Tools and Algorithms for the Construction and Analysis of Systems. Edinburgh, Scotland, April 2005. LNCS, No 3440. Springer.
fbk.eu