Roberto Bruttomesso
Roberto Bruttomesso
Expert Researcher and Software Engineer
Verified email at atrenta.com
Title
Cited by
Cited by
Year
The MathSAT 4 SMT Solver
R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani
International Conference on Computer Aided Verification, 299-303, 2008
2462008
The opensmt solver
R Bruttomesso, E Pek, N Sharygina, A Tsitovich
International Conference on Tools and Algorithms for the Construction and …, 2010
1372010
Efficient satisfiability modulo theories via delayed theory combination
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P Van Rossum, ...
International Conference on Computer Aided Verification, 335-349, 2005
1022005
A Lazy and Layered SMT() Solver for Hard Industrial Verification Problems
R Bruttomesso, A Cimatti, A Franzén, A Griggio, Z Hanna, A Nadel, A Palti, ...
International Conference on Computer Aided Verification, 547-560, 2007
972007
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
Journal of Automated Reasoning 35 (1-3), 265-293, 2005
952005
Efficient theory combination via boolean search
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P van Rossum, ...
Information and Computation 204 (10), 1493-1525, 2006
872006
An incremental and layered procedure for the satisfiability of linear arithmetic logic
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Tools and Algorithms for the Construction and …, 2005
872005
An incremental and layered procedure for the satisfiability of linear arithmetic logic
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Tools and Algorithms for the Construction and …, 2005
872005
The mathsat 3 system
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
International Conference on Automated Deduction, 315-321, 2005
692005
SAFARI: SMT-based abstraction for arrays with interpolants
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
International Conference on Computer Aided Verification, 679-685, 2012
572012
Lazy abstraction with interpolants for arrays
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
International Conference on Logic for Programming Artificial Intelligence …, 2012
512012
Encoding RTL constructs for MathSAT: a preliminary report
M Bozzano, R Bruttomesso, A Cimatti, A Franzén, Z Hanna, ...
Electronic Notes in Theoretical Computer Science 144 (2), 3-14, 2006
422006
The 2014 SMT competition
DR Cok, D Déharbe, T Weber
Journal on Satisfiability, Boolean Modeling and Computation 9 (1), 207-242, 2014
382014
An extension of lazy abstraction with interpolation for programs with arrays
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
Formal Methods in System Design 45 (1), 63-109, 2014
362014
Verifying heap-manipulating programs in an SMT framework
Z Rakamarić, R Bruttomesso, AJ Hu, A Cimatti
International Symposium on Automated Technology for Verification and …, 2007
332007
A scalable decision procedure for fixed-width bit-vectors
R Bruttomesso, N Sharygina
Proceedings of the 2009 International Conference on Computer-Aided Design, 13-20, 2009
322009
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis
R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani
International Conference on Logic for Programming Artificial Intelligence …, 2006
302006
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
R Bruttomesso, A Cimatti, A Franzen, A Griggio, R Sebastiani
Annals of Mathematics and Artificial Intelligence 55 (1-2), 63, 2009
272009
An efficient and flexible approach to resolution proof reduction
SF Rollini, R Bruttomesso, N Sharygina
Haifa verification conference, 182-196, 2010
262010
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in
R Bruttomesso, A Cimatti, A Franzén, A Griggio, A Santuari, R Sebastiani
International Conference on Logic for Programming Artificial Intelligence …, 2006
252006
The system can't perform the operation now. Try again later.
Articles 1–20