Roberto Bruttomesso

Available identifiers

zbMath Open bruttomesso.robertoMaRDI QIDQ479813

List of research outcomes

Publication	Date of Publication	Type
Resolution proof transformation for compression and interpolation	2014-12-05	Paper
An extension of lazy abstraction with interpolation for programs with arrays	2014-12-05	Paper
Quantifier-free interpolation in combinations of equality interpolating theories	2014-04-16	Paper
Encoding RTL constructs for \textsc{MathSAT}: a preliminary report	2013-09-26	Paper
From strong amalgamability to modularity of quantifier-free interpolation	2012-09-05	Paper
Lazy abstraction with interpolants for arrays	2012-06-15	Paper
Quantifier-free interpolation of a theory of arrays	2012-05-16	Paper
Rewriting-based quantifier-free interpolation for a theory of arrays	2012-04-24	Paper
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints	2011-10-07	Paper
An efficient and flexible approach to resolution proof reduction	2011-04-06	Paper
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis	2009-11-16	Paper
Verifying Heap-Manipulating Programs in an SMT Framework	2008-07-03	Paper
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis	2008-05-27	Paper
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$	2008-05-27	Paper
M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures	2007-01-24	Paper
Efficient theory combination via Boolean search	2006-10-25	Paper
Computer Aided Verification	2006-01-10	Paper
Tools and Algorithms for the Construction and Analysis of Systems	2005-11-10	Paper

Research outcomes over time

This page was built for person: Roberto Bruttomesso