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

The opensmt solver R Bruttomesso, E Pek, N Sharygina, A Tsitovich International Conference on Tools and Algorithms for the Construction and …, 2010 | 137 | 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 | 102 | 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 | 97 | 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-3), 265-293, 2005 | 95 | 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 | 87 | 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 | 87 | 2005 |

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 | 87 | 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 | 69 | 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 | 57 | 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 | 51 | 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 | 42 | 2006 |

The 2014 SMT competition DR Cok, D Déharbe, T Weber Journal on Satisfiability, Boolean Modeling and Computation 9 (1), 207-242, 2014 | 38 | 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 | 36 | 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 | 33 | 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 Franzén, A Griggio, R Sebastiani International Conference on Logic for Programming Artificial Intelligence …, 2006 | 30 | 2006 |

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 | 27 | 2009 |

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

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