Author name cluster

Roberto Bruttomesso

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

LPAR Conference 2012 Conference Paper

Lazy Abstraction with Interpolants for Arrays

Francesco Alberti
Roberto Bruttomesso
Silvio Ghilardi
Silvio Ranise
Natasha Sharygina

Abstract Lazy abstraction with interpolants has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method shows an intrinsic limitation, due to the fact that successful invariants usually contain universally quantified variables, which are not present in the program specification. In this work we present an extension of the interpolation-based lazy abstraction in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework, to derive a backward reachability version of lazy abstraction that embeds array reasoning. The approach is generic, in that it is valid for both parameterized systems and imperative programs. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.

Details

LPAR Conference 2006 Conference Paper

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis

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

Abstract Many approaches for Satisfiability Modulo Theory ( SMT \({\mathcal({T})})\) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory \({\mathcal{T}} ({\mathcal{T}}-solver\) ). When \({\mathcal{T}}\) is the combination \({{\mathcal{T}}_1\cup{\mathcal{T}}_2}\) of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific \({\mathcal{T}}\) - solver deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), called Delayed Theory Combination ( Dtc ). Here part or all the (possibly very expensive) task of deducing interface equalities is played by the SAT solver itself, at the potential cost of an enlargement of the boolean search space. In principle this enlargement could be up to exponential in the number of interface equalities generated. In this paper we show that this estimate was too pessimistic. We present a comparative analysis of Dtc vs. NO for SMT \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), which shows that, using state-of-the-art SAT-solving techniques, the amount of boolean branches performed by Dtc can be upper bounded by the number of deductions and boolean branches performed by NO on the same problem. We prove the result for different deduction capabilities of the \({\mathcal({T}-solver)}\) and for both convex and non-convex theories.

Details

I&C Journal 2006 Journal Article

Efficient theory combination via boolean search

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

Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T 1 ∪ T 2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e. g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT ( T 1 ∪ T 2 ), where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i. e. , cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions ( EUF ) and Linear Arithmetic ( LA ), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

Details DOI

LPAR Conference 2006 Conference Paper

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

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

Abstract Satisfiability Modulo Theories \((\mathit{SMT}(\mathcal{T}))\) is the problem of deciding the satisfiability of a formula with respect to a given background theory \({\mathcal{T}}\). When \({\mathcal{T}}\) is the combination of two simpler theories \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2} ({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})})\), a standard and general approach is to handle the integration of \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2}\) by performing some form of search on the equalities between the shared variables. A frequent and very relevant sub-case of \({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})}\) is when \({{\mathcal{T}}_1}\) is the theory of Equality and Uninterpreted Functions \(({\mathcal{EUF}})\). For this case, an alternative approach is to eliminate first all uninterpreted function symbols by means of Ackermann’s expansion, and then to solve the resulting \({\mathit{SMT}}({{\mathcal{T}}_2})\) problem. In this paper we build on the empirical observation that there is no absolute winner between these two alternative approaches, and that the performance gaps between them are often dramatic, in either direction. We propose a simple technique for estimating a priori the costs and benefits, in terms of the size of the search space of an \({\mathit{SMT}}\) tool, of applying Ackermann’s expansion to all or part of the function symbols. A thorough experimental analysis, including the benchmarks of the SMT’05 competition, shows that the proposed technique is extremely effective in improving the overall performance of the \({\mathit{SMT}}\) tool.

Details