Roberto Bruttomesso

Publication Activity (10 Years)

Years Active: 2005-2021
Publications (10 Years): 1

Top Topics

Rewrite Systems

Quantifier Free

Mutual Exclusion

Automatic Theorem Proving

Top Venues

Formal Methods Syst. Des.

ACM Trans. Comput. Log.

Publications

Roberto Bruttomesso
Intrepid: A Scriptable and Cloud-Ready SMT-Based Model Checker. FMICS (2021)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15 (1) (2014)
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45 (1) (2014)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45 (1) (2014)
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
Resolution Proof Transformation for Compression and Interpolation. CoRR (2013)
Roberto Bruttomesso, Alberto Griggio
Broadening the Scope of SMT-COMP: the Application Track. COMPARE (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Lazy Abstraction with Interpolants for Arrays. LPAR (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Reachability Modulo Theory Library. SMT@IJCAR (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR (2012)
Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Quantifier-Free Interpolation of a Theory of Arrays Log. Methods Comput. Sci. 8 (2) (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation CoRR (2012)
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV (2012)
David R. Cok, Alberto Griggio, Roberto Bruttomesso, Morgan Deters
The 2012 SMT Competition. SMT@IJCAR (2012)
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA (2011)
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)
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich
The OpenSMT Solver. TACAS (2010)
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
A flexible schema for generating explanations in lazy theory propagation. MEMOCODE (2010)
Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich
Flexible interpolation with local proof transformations. ICCAD (2010)
Simone Rollini, Roberto Bruttomesso, Natasha Sharygina
An Efficient and Flexible Approach to Resolution Proof Reduction. Haifa Verification Conference (2010)
Roberto Bruttomesso, Natasha Sharygina
A scalable decision procedure for fixed-width bit-vectors. ICCAD (2009)
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) (2009)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
The MathSAT 4SMT Solver. CAV (2008)
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)
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti
Verifying Heap-Manipulating Programs in an SMT Framework. ATVA (2007)
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)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
). LPAR (2006)
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. Electron. Notes Theor. Comput. Sci. 144 (2) (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) (2006)
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
The MathSAT 3 System. CADE (2005)
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. Reason. 35 (1-3) (2005)
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)
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)