Showing 1–4 of 4 results for author: Alberti, F

Counting Constraints in Flat Array Fragments

Authors: Francesco Alberti, Silvio Ghilardi, Elena Pagani

Abstract: We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a fragment and we implement our algorithms. The experiments run in discharging proof obligations coming from invariant checking and bounded model-checking benchmarks s… ▽ More We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a fragment and we implement our algorithms. The experiments run in discharging proof obligations coming from invariant checking and bounded model-checking benchmarks show the practical feasibility of our decision procedure. △ Less

Submitted 1 February, 2016; originally announced February 2016.

A simple abstraction of arrays and maps by program translation

Authors: David Monniaux, Francesco Alberti

Abstract: We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpreta… ▽ More We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.. .). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the " Dutch flag " algorithm. △ Less

Submitted 12 June, 2015; originally announced June 2015.

Monotonic Abstraction Techniques: from Parametric to Software Model Checking

Authors: Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Abstract: Monotonic abstraction is a technique introduced in model checking parameterized distributed systems in order to cope with transitions containing global conditions within guards. The technique has been re-interpreted in a declarative setting in previous papers of ours and applied to the verification of fault tolerant systems under the so-called "stop** failures" model. The declarative reinterpret… ▽ More Monotonic abstraction is a technique introduced in model checking parameterized distributed systems in order to cope with transitions containing global conditions within guards. The technique has been re-interpreted in a declarative setting in previous papers of ours and applied to the verification of fault tolerant systems under the so-called "stop** failures" model. The declarative reinterpretation consists in logical techniques (quantifier relativizations and, especially, quantifier instantiations) making sense in a broader context. In fact, we recently showed that such techniques can over-approximate array accelerations, so that they can be employed as a meaningful (and practically effective) component of CEGAR loops in software model checking too. △ Less

Submitted 13 November, 2014; originally announced November 2014.

Comments: In Proceedings MOD* 2014, arXiv:1411.3453

Journal ref: EPTCS 168, 2014, pp. 1-11

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs

Authors: Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Abstract: Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence phenomena in a satisfactory way. Acceleration is an approach which is widely used to avoid divergence, but it has been applied mostly to integer programs. This paper addresses the problem of accelerating transition rela… ▽ More Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence phenomena in a satisfactory way. Acceleration is an approach which is widely used to avoid divergence, but it has been applied mostly to integer programs. This paper addresses the problem of accelerating transition relations for unbounded arrays with the ultimate goal of avoiding divergence during reachability analysis of abstract programs. For this, we first design a format to compute accelerations in this domain; then we show how to adapt the so-called 'monotonic abstraction' technique to efficiently handle complex formulas with nested quantifiers generated by the acceleration preprocessing. Notably, our technique can be easily plugged-in into abstraction/refinement loops, and strongly contributes to avoid divergence: experiments conducted with the MCMT model checker attest the effectiveness of our approach on programs with unbounded arrays, where acceleration and abstraction/refinement technologies fail if applied alone. △ Less

Submitted 3 October, 2013; v1 submitted 16 April, 2013; originally announced April 2013.

Comments: Published in the proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS) with the title "Definability of Accelerated Relations in a Theory of Arrays and its Applications" (available at http://www.springerlink.com)