the eureka software model checker is part of the eureka project at artificial intelligence laboratory

eureka is an effective model checker for C programs that follows the counterexample guided abstraction refinement schema. Instead of using the common boolean programs as an abstract model, we use linear programs: similarly to boolean programs, linear programs have the usual control-flow constructs and procedural abstraction with call-by-value parameter passing and recursion. linear programs differ from boolean programs in that program variables range over a numeric domain (e.g. the integers or the reals); moreover, all conditions and assignments to variables involve linear expressions, i.e. expressions of the form c0+c1*x1+...+cn*xn, where c0,...,cn are numeric constants and x1,...,xn are program variables ranging over a numeric domain. linear programs are considerably more accurate than boolean programs and can encode explicitly complex correlations between data and control that must necessarily be abstracted away when using boolean programs.

At the current stage of development, the eureka tool is capable to verify Linear Programs with Arrays (i.e. Linear Programs augmented with references to array elements of numeric type) by abstracting away array elements that are not needed to verify a given property. If the abstract trace exhibited by the model checker is not feasible in the original program, new array indexes are added in order to refine the model. For more details, please go to the papers section of the eureka project web page.

You may want to take a look at the benchmark programs that we used for our experiments and at the results we obtained. The tarball below contains the C files that have been tested against two state-of-the art model checkers, namely BLAST and CBMC. The results are summarized in the following table:

-----------------------------------------------------
PROGRAM                      EUREKA   BLAST    CBMC
-----------------------------------------------------
array_init.c                 safe     error    safe 
array_init_assign.c          safe     unsafe   safe
complex_guard.c              safe     unsafe   safe
simple_swap.c                safe     safe     safe
sequential_swap_call.c       safe     error    safe
simple_array_inversion.c     safe     unsafe   safe
bubblesort_inner_loop.c      unsafe   error    unsafe
bubblesort.c                 unsafe   safe     unsafe
array_max.c                  safe     error    safe
wrong_loop.c                 unsafe   error    mout
loop_on_input.c              unsafe   unsafe   mout
simple_control_on_input.c    unsafe   unsafe   mout
-----------------------------------------------------