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 | 284 | 2008 |

The opensmt solver R Bruttomesso, E Pek, N Sharygina, A Tsitovich International Conference on Tools and Algorithms for the Construction and …, 2010 | 157 | 2010 |

Efficient satisfiability modulo theories via delayed theory combination M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P Rossum, ... International Conference on Computer Aided Verification, 335-349, 2005 | 110 | 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 | 103 | 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 | 101 | 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 | 92 | 2006 |

An incremental and layered procedure for the satisfiability of linear arithmetic logic M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Rossum, S Schulz, ... International Conference on Tools and Algorithms for the Construction and …, 2005 | 92 | 2005 |

An incremental and layered procedure for the satisfiability of linear arithmetic logic M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Rossum, S Schulz, ... International Conference on Tools and Algorithms for the Construction and …, 2005 | 92 | 2005 |

The mathsat 3 system M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Rossum, S Schulz, ... International Conference on Automated Deduction, 315-321, 2005 | 75 | 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 | 65 | 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 | 55 | 2012 |

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 | 50 | 2006 |

The 2014 SMT competition DR Cok, D Déharbe, T Weber Journal on Satisfiability, Boolean Modeling and Computation 9 (1), 207-242, 2014 | 46 | 2014 |

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 | 43 | 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 | 35 | 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 | 32 | 2009 |

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 | 31 | 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 | 30 | 2006 |

Quantifier-free interpolation of a theory of arrays R Bruttomesso, S Ghilardi, S Ranise arXiv preprint arXiv:1204.2386, 2012 | 28 | 2012 |

An efficient and flexible approach to resolution proof reduction SF Rollini, R Bruttomesso, N Sharygina Haifa verification conference, 182-196, 2010 | 27 | 2010 |