SAFARI: SMT-based abstraction for arrays with interpolants

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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æ for symbolically representing states. A heuristics, called term abstraction, favors the convergence of the tool by "tuning" interpolants and guessing additional quantified variables of invariants to prune the search space efficiently.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages679-685
Number of pages7
Volume7358 LNCS
DOIs
Publication statusPublished - 2012
Event24th International Conference on Computer Aided Verification, CAV 2012 - Berkeley, CA, United States
Duration: Jul 7 2012Jul 13 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7358 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other24th International Conference on Computer Aided Verification, CAV 2012
CountryUnited States
CityBerkeley, CA
Period7/7/127/13/12

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'SAFARI: SMT-based abstraction for arrays with interpolants'. Together they form a unique fingerprint.

  • Cite this

    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., & Sharygina, N. (2012). SAFARI: SMT-based abstraction for arrays with interpolants. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 679-685). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS). https://doi.org/10.1007/978-3-642-31424-7_49