Eureka: Model Checking Programs Manipulating Numerical Data and Arrays

Eureka is a model checker for programs manipulating numerical data and arrays. Eureka leverages the Counterexample-guided Abstraction Refinement (CEGAR) paradigm as well as a novel abstraction technique tailored to reason about arrays. Eureka is the result of a joint effort of the AI-Lab at the University of Genova and the Section of Computer Science, Physical Sciences Department at the University of Napoli "Federico II". Eureka has been partly supported by the Italian Ministry of University and Research, in the context of the PRIN Project no. 2003-097383.

Overview

The CEGAR Loop Counterexample-guided Abstraction Refinement based on predicate abstraction is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. Eureka implements a novel CEGAR procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In Eureka the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the tools based on predicate abstraction, Eureka treats arrays precisely. This is an important feature as arrays are ubiquitous in programming.

The Eureka Tool

Eureka supports reasoning about numberical data and arrays as well as a wide range of features occurring in modern imperative languages, including (arbitrarily nested) loops, non-determinism, procedure calls and recursion. If an error is found, Eureka exhibits an error trace, i.e. a sequence of statements whose execution leads to an assertion violation. Eureka currently does not support the analysis of programs with pointers, dynamically allocated arrays, bit-level constructs, unbounded arrays or arrays with symbolic dimensions.

Architectural View of Eureka The architecture of Eureka is depicted in the figure on the right. The Model Checking procedure analyses Linear Programs (without arrays) by treating arithmetic natively. This is done by leveraging the powerful functionalities of the Parma Polyhedra Library (PPL). By using the PPL sets of reachable states are represented and efficiently handled by PPL as polyhedra. Whenever the model checker finds an error trace in the abstract program, then the Simulate module builds a formula whose satisifability corresponds to the executability of the same trace in the original program. The feasibility of the formula is then checked by invoking an SMT-solver. Eureka uses CVC Lite to this end. If the formula is found to be satisfiable, then Eureka terminates and reports the error trace. Otherwise, the proof of unsatisfiability generated by CVC Lite is inspected to determine a set of array indexes to be used to refine the abstract program. This step is such that the new, abstract program is is more precise than the previous abstraction and does not contain the spurious error trace found by the Model Checking phase.

Experimental Evalutation

We have run Eureka and a number of state-of-the-art software model checkers (Blast, SATABS, and CPAchecker) against a variety of problems that involve reasoning on arithmetics and/or arrays. This allowed us to comparatively evaluate the effectiveness of the software model checking procedures implemented in the tools. A detailed description of benchmarks and of the experimental evaluation can be found in this paper. The benchmarks and the log files generated by the tools during the experiments can be downloaded from this link.

Publications

People

The following people contributed to the development of Eureka: