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
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
- Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
- Shimizu, Hiroaki; Hamaguchi, Kiyoharu; Kashiwabara, Toshinobu: Approximate invariant property checking using term-height reduction for a subset of first-order logic (2008)