IRIS

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. © 2012 Springer-Verlag.

SAFARI: SMT-based abstraction for arrays with interpolants / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - 7358:(2012), pp. 679-685. (Intervento presentato al convegno 24th International Conference on Computer Aided Verification, CAV 2012 tenutosi a Berkeley, CA, usa nel 2012) [10.1007/978-3-642-31424-7_49].

SAFARI: SMT-based abstraction for arrays with interpolants

Ranise S.;
2012-01-01

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. © 2012 Springer-Verlag.
2012
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-642-31423-0
978-3-642-31424-7
2-s2.0-84864059309
Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.
SAFARI: SMT-based abstraction for arrays with interpolants / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - 7358:(2012), pp. 679-685. (Intervento presentato al convegno 24th International Conference on Computer Aided Verification, CAV 2012 tenutosi a Berkeley, CA, usa nel 2012) [10.1007/978-3-642-31424-7_49].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/332979
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 34
  • ???jsp.display-item.citation.isi??? ND
social impact