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.

• Type: Conference
• Year: 2007
• Where: KBSE
• Authors: Alessandro Armando, Massimo Benerecetti, Dario Carotenuto, Jacopo Mantovani, Pasquale Spica
• Keywords: Array Elements, KBSE 2007, Linear Programs, Software Engineering, Symbolic Model Checker