SAFARI

SAFARI - SMT-based Abstraction For Arrays with Interpolants - is a model checker designed to prove safety (possibly universally quantified) properties of imperative programs with arrays. SAFARI is based on an extension of the Lazy Abstraction paradigm capable of handling existentially quantified formulae by using a combination of quantifier-free interpolation algorithms for the indexes and elements in the arrays during refinement. A heuristics, called term abstraction, augments the convergence of the tool by "tuning" interpolants and guessing additional quantified variables of invariants to prune the search space.

More information about the integration of the Lazy Abstraction paradigm with the Model Checking Modulo Theories paradigm can be found on [1].

SAFARI will be presented at CAV 2012. More informations on [2].

References

  1. Lazy Abstraction with Interpolants for Arrays, Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N. , 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), Mérida, Venezuela, Springer (2012)
  2. SAFARI: SMT-based Abstraction For Arrays with Interpolants, Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N. , 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, Springer (2012)