Roberto Bruttomesso

33 papers A* 4A 6B 4C 2Journal 9Unranked 8
YearRankTypeTitle / Venue / Authors
2021 C conf
Intrepid: A Scriptable and Cloud-Ready SMT-Based Model Checker.
FMICS
Roberto Bruttomesso
2014 J jnl
An extension of lazy abstraction with interpolation for programs with arrays.
Formal Methods Syst. Des.
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2014 J jnl
Quantifier-free interpolation in combinations of equality interpolating theories.
ACM Trans. Comput. Log.
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2014 J jnl
Resolution proof transformation for compression and interpolation.
Formal Methods Syst. Des.
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
2013 J jnl
Resolution Proof Transformation for Compression and Interpolation.
CoRR
Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich
2012 — conf
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms.
NASA Formal Methods
Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise
2012 — conf
Broadening the Scope of SMT-COMP: the Application Track.
COMPARE
Roberto Bruttomesso, Alberto Griggio
2012 J jnl
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
CoRR
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012 A conf
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation.
IJCAR
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012 B conf
Lazy Abstraction with Interpolants for Arrays.
LPAR
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012 J jnl
Quantifier-Free Interpolation of a Theory of Arrays
Log. Methods Comput. Sci.
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2012 — conf
Reachability Modulo Theory Library.
SMT@IJCAR
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012 A* conf
SAFARI: SMT-Based Abstraction for Arrays with Interpolants.
CAV
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
2012 — conf
The 2012 SMT Competition.
SMT@IJCAR
David R. Cok, Alberto Griggio, Roberto Bruttomesso, Morgan Deters
2011 — conf
A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints.
FroCoS
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2011 — conf
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
RTA
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
2010 C conf
A flexible schema for generating explanations in lazy theory propagation.
MEMOCODE
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina
2010 — conf
An Efficient and Flexible Approach to Resolution Proof Reduction.
Haifa Verification Conference
Simone Rollini, Roberto Bruttomesso, Natasha Sharygina
2010 A conf
Flexible interpolation with local proof transformations.
ICCAD
Roberto Bruttomesso, Simone Rollini, Natasha Sharygina, Aliaksei Tsitovich
2010 A conf
The OpenSMT Solver.
TACAS
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich
2009 A conf
A scalable decision procedure for fixed-width bit-vectors.
ICCAD
Roberto Bruttomesso, Natasha Sharygina
2009 J jnl
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.
Ann. Math. Artif. Intell.
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2008 A* conf
The MathSAT 4SMT Solver.
CAV
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2007 A* conf
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.
CAV
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani
2007 B conf
Verifying Heap-Manipulating Programs in an SMT Framework.
ATVA
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti
2006 B conf
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis.
LPAR
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2006 J jnl
Efficient theory combination via boolean search.
Inf. Comput.
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2006 B conf
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in
LPAR
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
2005 A conf
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.
TACAS
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005 A* conf
Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
CAV
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2005 — conf
Encoding RTL Constructs for MathSAT: a Preliminary Report.
PDPAR@CAV
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani
2005 J jnl
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.
J. Autom. Reason.
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005 A conf
The MathSAT 3 System.
CADE
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani