Author name cluster

Alberto Griggio

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.

7 papers

2 author rows

I&C Journal 2022 Journal Article

LTL falsification in infinite-state systems

Alessandro Cimatti
Alberto Griggio
Enrico Magnago

In finite-state systems, if an LTL property is false, there is always a counterexample path (i. e. a witness) for it which is ultimately periodic (i. e. in a lasso-shaped form). When dealing with infinite-state systems, this is no longer the case. In this work, we address this issue by proposing an automatic approach that presents witnesses in an indirect way. The approach is based on two key insights. First, we leverage the notion of well-founded funnel, where a ranking function ensures that the states in the source set are guaranteed to inevitably reach the destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. Second, we adopt a compositional approach to partition the original system into projections and to prove that they result in a non-empty under-approximation of the original system that only contains fair paths. Then, we propose an algorithm that, working in an abstract space induced by a set of predicates, identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order. We experimentally evaluate the approach on examples taken from software, timed and hybrid systems, showing its wide applicability and expressiveness, with an implementation that outperforms various competitor tools.

Details DOI

I&C Journal 2020 Journal Article

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

Alessandro Cimatti
Alberto Griggio
Enrico Magnago
Marco Roveri
Stefano Tonetta

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL 0, ∞ with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in the nuXmv model checker enabling the analysis of LTL-EF and MTL 0, ∞ based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

Details DOI

SAT Conference 2018 Conference Paper

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

Alessandro Cimatti
Alberto Griggio
Ahmed Irfan
Marco Roveri
Roberto Sebastiani

Abstract Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

Details

SAT Conference 2013 Conference Paper

A Modular Approach to MaxSAT Modulo Theories

Alessandro Cimatti
Alberto Griggio
Bastiaan Joost Schaafsma
Roberto Sebastiani

Abstract In this paper we present a novel “modular” approach for (weighted partial) MaxSAT Modulo Theories. The main idea is to combine a lazy SMT solver with a purely-propositional (weighted partial) MaxSAT solver, by making them exchange information iteratively: the former produces an increasing set of theory lemmas which are used by the latter to progressively refine an approximation of the final subset of the soft clauses, which is eventually returned as output. The approach has several practical features. First, it is independent from the theories addressed. Second, it is simple to implement and to update, since both SMT and MaxSAT solvers can be used as blackboxes. Third, it can be interfaced with external MaxSAT and SMT solvers in a plug-and-play manner, so that to benefit for free of tools which are or will be made available. We have implemented our approach on top of the MathSAT5 SMT solver and of a selection of external MaxSAT solvers, and we have evaluated it by means of an extensive empirical test on SMT-LIB benchmarks. The results confirm the validity and potential of this approach.

Details

SAT Conference 2007 Conference Paper

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories

Alessandro Cimatti
Alberto Griggio
Roberto Sebastiani

Abstract Finding small unsatisfiable cores for SAT problems has recently received a lot of interest, mostly for its applications in formal verification. Surprisingly, the same problem in the context of SAT Modulo Theories (SMT) has instead received very little attention in the literature; in particular, we are not aware of any work aiming at producing small unsatisfiable cores in SMT. The purpose of this paper is to start filling the gap in this area, by proposing a novel approach for computing small unsat cores in SMT. The main idea is to combine an SMT solver with an external propositional core extractor: the SMT solver produces the theory lemmas found during the search; the core extractor is then called on the boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas have been removed. The approach has several advantages: it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play way, so that to benefit for free of all unsat-core reduction techniques which have been or will be made available.

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

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