| 2008 |
|---|
| 7 | EE | Roberto Bruttomesso,
Alessandro Cimatti,
Anders Franzén,
Alberto Griggio,
Roberto Sebastiani:
The MathSAT 4SMT Solver.
CAV 2008: 299-303 |
| 2007 |
|---|
| 6 | EE | Roberto Bruttomesso,
Alessandro Cimatti,
Anders Franzén,
Alberto Griggio,
Ziyad Hanna,
Alexander Nadel,
Amit Palti,
Roberto Sebastiani:
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.
CAV 2007: 547-560 |
| 5 | EE | Roberto Cavada,
Alessandro Cimatti,
Anders Franzén,
Krishnamani Kalyanasundaram,
Marco Roveri,
R. K. Shyamasundar:
Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.
FMCAD 2007: 69-76 |
| 2006 |
|---|
| 4 | EE | Roberto Bruttomesso,
Alessandro Cimatti,
Anders Franzén,
Alberto Griggio,
Roberto Sebastiani:
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis.
LPAR 2006: 527-541 |
| 3 | EE | 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 ÈT).
LPAR 2006: 557-571 |
| 2 | EE | Anders Franzén:
Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs.
Electr. Notes Theor. Comput. Sci. 144(1): 19-33 (2006) |
| 1 | EE | Marco Bozzano,
Roberto Bruttomesso,
Alessandro Cimatti,
Anders Franzén,
Ziyad Hanna,
Zurab Khasidashvili,
Amit Palti,
Roberto Sebastiani:
Encoding RTL Constructs for MathSAT: a Preliminary Report.
Electr. Notes Theor. Comput. Sci. 144(2): 3-14 (2006) |
