Bruttomesso, Roberto
Bruttomesso, Roberto
A lazy and layered SMT(BV) solver for hard industrial verification problems
2007-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Z., Hanna; A., Nadel; A., Palti; Sebastiani, Roberto
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic
2005-01-01 M., Bozzano; Bruttomesso, Roberto; Cimatti, Alessandro; T., Junttila; P., Van Rossum; Sebastiani, Roberto; S., Schulz
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis
2006-01-01 Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis
2006-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Sebastiani, Roberto
Delayed Theory Combination vs. Nelson-oppen for satisfiability modulo theories: A comparative analysis
2009-01-01 Bruttomesso, Roberto; Cimatti, Alessandro; A., Franzen; Griggio, Alberto; Sebastiani, Roberto
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version
2009-01-01 Bruttomesso, Roberto; Cimatti, Alessandro; Anders, Franzen; Griggio, Alberto; Sebastiani, Roberto
Efficient Satisfiability Modulo Theories via Delayed Theory Combination
2005-01-01 Bozzano, M.; Bruttomesso, Roberto; Cimatti, A.; Junttila, T.; Van Rossum, P.; Ranise, S.; Sebastiani, Roberto
Efficient theory combination via Boolean search
2006-01-01 Bozzano, M.; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, T.; Van Rossum, P.; Ranise, S.; Sebastiani, Roberto
Encoding RTL Constructs for MathSAT: a Preliminary Report
2006-01-01 M., Bozzano; Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Z., Hanna; Z., Khasidashvili; A., Palti; Sebastiani, Roberto
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures
2005-01-01 M., Bozzano; Bruttomesso, Roberto; Cimatti, Alessandro; T., Junttila; P., Van Rossum; S., Schulz; Sebastiani, Roberto
The MathSAT 3 System
2005-01-01 M., Bozzano; Bruttomesso, Roberto; T., Junttila; S., Schulz; Sebastiani, Roberto; P., Var Rossum
The MathSAT 4 SMT Solver
2008-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Sebastiani, Roberto
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT (EUF ÈT)
2006-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; A., Santuari; Sebastiani, Roberto
To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T)
2006-01-01 Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto