@article {216, title = {Decision Procedures for Flat Array Properties}, journal = {J. Autom. Reasoning}, volume = {54}, year = {2015}, month = {04/2015}, pages = {352}, chapter = {327}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {221, title = {A new Acceleration-based Combination Framework for Array Properties}, booktitle = {FROCOS 2015}, year = {2015}, author = {Francesco Alberti and Silvio Ghilardi and Natasha Sharygina} } @mastersthesis {219, title = {An SMT-based verification framework for software systems handling arrays}, volume = {PhD}, year = {2015}, month = {02/2015}, pages = {188}, school = {Universit{\`a} della Svizzera Italiana}, type = {Doctoral Dissertation}, address = {Lugano}, url = {http://www.falberti.it/thesis/phd.pdf}, author = {Francesco Alberti} } @conference {185, title = {Decision Procedures for Flat Array Properties}, booktitle = {TACAS}, year = {2014}, publisher = {Springer}, organization = {Springer}, address = {Grenoble, France}, 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 an prove universally quantified properties over arrays in a completely automatic fashion.
}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @conference {151, title = {SAFARI: SMT-based Abstraction For Arrays with Interpolants}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {We present SAFARI, a model checker designed to prove (possibly universally quantified) safety properties of imperative programs with arrays of unknown length. SAFARI is based on an extension of lazy abstraction capable of handling existentially quantified formul{\ae} for symbolically representing states. A heuristics, called term abstraction, favors the convergence of the tool by {\textquotedblleft}tuning{\textquotedblright} interpolants and guessing additional quantified variables of invariants to prune the search space efficiently.
}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} }