Roberto Bruttomesso

According to our database, Roberto Bruttomesso authored at least 30 papers between 2005 and 2021.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2021

Intrepid: A Scriptable and Cloud-Ready SMT-Based Model Checker.

Roberto Bruttomesso

Proceedings of the Formal Methods for Industrial Critical Systems, 2021

2014

Quantifier-free interpolation in combinations of equality interpolating theories.

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

ACM Trans. Comput. Log., 2014

Resolution proof transformation for compression and interpolation.

Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich

Formal Methods Syst. Des., 2014

An extension of lazy abstraction with interpolation for programs with arrays.

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Formal Methods Syst. Des., 2014

2012

Quantifier-Free Interpolation of a Theory of Arrays

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Log. Methods Comput. Sci., 2012

Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms.

Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise

Proceedings of the NASA Formal Methods, 2012

Lazy Abstraction with Interpolants for Arrays.

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

SAFARI: SMT-Based Abstraction for Arrays with Interpolants.

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

The 2012 SMT Competition.

David R. Cok, Alberto Griggio, Roberto Bruttomesso, Morgan Deters

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

From Strong Amalgamability to Modularity of Quantifier-Free Interpolation.

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Broadening the Scope of SMT-COMP: the Application Track.

Roberto Bruttomesso, Alberto Griggio

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Reachability Modulo Theory Library.

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints.

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

The OpenSMT Solver.

Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

A flexible schema for generating explanations in lazy theory propagation.

Roberto Bruttomesso, Edgar Pek, Natasha Sharygina

Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Flexible interpolation with local proof transformations.

Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich

Proceedings of the 2010 International Conference on Computer-Aided Design, 2010

An Efficient and Flexible Approach to Resolution Proof Reduction.

Simone Rollini, Roberto Bruttomesso, Natasha Sharygina

Proceedings of the Hardware and Software: Verification and Testing, 2010

2009

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani

Ann. Math. Artif. Intell., 2009

A scalable decision procedure for fixed-width bit-vectors.

Roberto Bruttomesso, Natasha Sharygina

Proceedings of the 2009 International Conference on Computer-Aided Design, 2009

2008

The MathSAT 4SMT Solver.

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Verifying Heap-Manipulating Programs in an SMT Framework.

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti

Proceedings of the Automated Technology for Verification and Analysis, 2007

2006

Efficient theory combination via boolean search.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani

Inf. Comput., 2006

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in <i>SMT</i>(<i>EUF</i> È<i>T</i>).

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani

Proceedings of the Logic for Programming, 2006

2005

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani

J. Autom. Reason., 2005

Encoding RTL Constructs for MathSAT: a Preliminary Report.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The MathSAT 3 System.

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani

Proceedings of the Automated Deduction, 2005