The eureka tool for software model checking
Alessandro Armando, Massimo Benerecetti, Dario Carotenuto, Jacopo Mantovani, Pasquale Spica · 2007
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.