| The MathSAT 4 SMT Solver: Tool Paper R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani International Conference on Computer Aided Verification, 299-303, 2008 | 316 | 2008 |
| The opensmt solver R Bruttomesso, E Pek, N Sharygina, A Tsitovich International Conference on TOOLS and Algorithms for the Construction and …, 2010 | 202 | 2010 |
| 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 | 116 | 2005 |
| 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 | 115 | 2007 |
| 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 | 106 | 2005 |
| 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 | 101 | 2006 |
| 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 | 98 | 2005 |
| 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 | 78 | 2005 |
| 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 | 74 | 2012 |
| 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 | 73 | 2012 |
| The 2014 SMT competition DR Cok, D Déharbe, T Weber Journal on Satisfiability, Boolean Modelling and Computation 9 (1), 207-242, 2014 | 65 | 2014 |
| 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 | 54 | 2006 |
| 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 | 46 | 2014 |
| 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 | 39 | 2007 |
| 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 | 38 | 2009 |
| 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 | 37 | 2014 |
| Quantifier-free interpolation of a theory of arrays R Bruttomesso, S Ghilardi, S Ranise Logical Methods in Computer Science 8, 2012 | 34 | 2012 |
| 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 | 32 | 2009 |
| 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 | 31 | 2006 |
| An efficient and flexible approach to resolution proof reduction SF Rollini, R Bruttomesso, N Sharygina Haifa verification conference, 182-196, 2010 | 28 | 2010 |
Alessandro CimattiFondazione Bruno KesslerVerified email at fbk.eu
