Roberto Bruttomesso

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Quantifier-Free Interpolation of a Theory of Arrays. Logical Methods in Computer Science 8(2) (2012)

Roberto Bruttomesso, Alberto Griggio: Broadening the Scope of SMT-COMP: the Application Track. COMPARE 2012: 18-27

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR 2012: 118-133

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina: SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV 2012: 679-685

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina: Lazy Abstraction with Interpolants for Arrays. LPAR 2012: 46-61

Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods 2012: 279-294

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. CoRR abs/1203.3730 (2012)

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. FroCoS 2011: 103-118

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA 2011: 171-186

Simone Rollini, Roberto Bruttomesso, Natasha Sharygina: An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference 2010: 182-196

Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich: Flexible interpolation with local proof transformations. ICCAD 2010: 770-777

Roberto Bruttomesso, Edgar Pek, Natasha Sharygina: A flexible schema for generating explanations in lazy theory propagation. MEMOCODE 2010: 41-48

Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich: The OpenSMT Solver. TACAS 2010: 150-153

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1-2): 63-99 (2009)

Roberto Bruttomesso, Natasha Sharygina: A scalable decision procedure for fixed-width bit-vectors. ICCAD 2009: 13-20

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: The MathSAT 4SMT Solver. CAV 2008: 299-303

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Verifying Heap-Manipulating Programs in an SMT Framework. ATVA 2007: 237-252

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani: A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV 2007: 547-560

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani: Encoding RTL Constructs for MathSAT: a Preliminary Report. Electr. Notes Theor. Comput. Sci. 144(2): 3-14 (2006)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR 2006: 527-541

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). LPAR 2006: 557-571

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reasoning 35(1-3): 265-293 (2005)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: The MathSAT 3 System. CADE 2005: 315-321

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333