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.
SAFARI: SMT-based Abstraction For Arrays with Interpolants / F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, N. Sharygina - In: Computer Aided Verification / [a cura di] P. Madhusudan, S. A. Seshia. - [s.l] : Springer, 2012. - ISBN 978-3-642-31423-0. - pp. 679-685 (( Intervento presentato al 24. convegno Computer Aided Verification tenutosi a Berkeley, CA, USA nel 2012 [10.1007/978-3-642-31424-7_49].
SAFARI: SMT-based Abstraction For Arrays with Interpolants
S. Ghilardi;
2012
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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
