The Eureka Tool for Software Model Checking. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element