The eureka tool for software model checking

Alessandro Armando, Massimo Benerecetti, Dario Carotenuto, Jacopo Mantovani, Pasquale Spica

Abstract

We describe EUREKA, a symbolic model checker for Linear Programs with arrays, i.e. programs where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. This language fragment easily encodes a large class of programs for which, as demonstrated by our experiments, techniques based on predicate abstraction do not apply successfully.

BibTeX

@inproceedings{Armando-al:ASE07,
  author    = {Alessandro Armando and
               Massimo Benerecetti and
               Dario Carotenuto and
               Jacopo Mantovani and
               Pasquale Spica},
  title     = {The eureka tool for software model checking},
  booktitle = {ASE},
  pages     = {541--542},
  publisher = {{ACM}},
  year      = {2007},
}

The eureka tool for software model checking

Abstract

Related papers