@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 {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} }