Follow
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: Tool Paper
R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani
Computer Aided Verification: 20th International Conference, CAV 2008 …, 2008
3042008
The opensmt solver
R Bruttomesso, E Pek, N Sharygina, A Tsitovich
Tools and Algorithms for the Construction and Analysis of Systems: 16th …, 2010
1822010
Efficient satisfiability modulo theories via delayed theory combination
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P Van Rossum, ...
Computer Aided Verification: 17th International Conference, CAV 2005 …, 2005
1132005
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
1072007
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), 265-293, 2005
1042005
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, ...
Tools and Algorithms for the Construction and Analysis of Systems: 11th …, 2005
962005
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
942006
The mathsat 3 system
M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ...
Automated Deduction–CADE-20: 20th International Conference on Automated …, 2005
782005
SAFARI: SMT-Based Abstraction for Arrays with Interpolants
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
Computer Aided Verification: 24th International Conference, CAV 2012 …, 2012
692012
Lazy abstraction with interpolants for arrays
F Alberti, R Bruttomesso, S Ghilardi, S Ranise, N Sharygina
Logic for Programming, Artificial Intelligence, and Reasoning: 18th …, 2012
662012
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
512006
The 2014 SMT competition
DR Cok, D Déharbe, T Weber
Journal on Satisfiability, Boolean Modeling and Computation 9 (1), 207-242, 2014
492014
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, 63-109, 2014
462014
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
362009
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
362007
Quantifier-free interpolation in combinations of equality interpolating theories
R Bruttomesso, S Ghilardi, S Ranise
ACM Transactions on Computational Logic (TOCL) 15 (1), 1-34, 2014
332014
Quantifier-free interpolation of a theory of arrays
R Bruttomesso, S Ghilardi, S Ranise
Logical Methods in Computer Science 8, 2012
332012
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), 63-99, 2009
312009
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
An efficient and flexible approach to resolution proof reduction
SF Rollini, R Bruttomesso, N Sharygina
Hardware and Software: Verification and Testing: 6th International Haifa …, 2011
282011
The system can't perform the operation now. Try again later.
Articles 1–20