This is the empirical evaluation of the implementation of our techniques from the paper Accelerating Loops with Arrays in our tool LoAT.

Getting LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Moreover, you can find the source code of LoAT at GitHub.

We refer to the general LoAT website for further information.

Evaluation

Examples

We used the C programs from the category ReachSafety-Arrays from the Software Verification Competition for our evaluation. To this end, we converted them to LoAT's input format (Constrained Horn Clauses, CHCs) using our novel tool HornKlaus. Currently, HornKlaus supports the fragment of C that corresponds to the CHCs supported by LoAT. So in particular, it does not support pointers, structs, or bit-wise operations. Thus, it can only transform 201 of the 439 SV-COMP benchmarks into CHCs, resulting in our first collection of benchmarks, called SV. However, the majority of these benchmarks is satsifiable, but the main purpose of our approach is proving unsatisfiability. To obtain more unsatisfiable instances, we modified HornKlaus so that it negates the assertions that characterize the error states, resulting in our second set of benchmarks, called SV_neg.

Tools

In our evaluation, we considered the following tools and configurations:

• LoAT's implementation of Accelerated Bounded Model Checking, which uses our novel acceleration technique
• loat-static --mode safety --engine abmc $INPUT
• LoAT's implementation of Accelerated Bounded Model Checking without our novel acceleration technique as baseline
• loat-static --mode safety --engine abmc --accel::arrays false $INPUT
• Z3's implementation of Bounded Model Checking (version 4.15.4)
• z3 fp.engine=bmc $INPUT
• Golem's implementation of Symbolic Execution (version 0.9.0)
• golem -e se $INPUT
• Eldarica's default configuration (version 2.2.1)
• eld $INPUT

Results

Here you can find a table with the detailed results of our benchmarks on the examples SV, and here you can find a table with the detailed results of our benchmarks on the examples SV_neg. Unique results (where all but one solver failed) are highlighted in yellow.

Running Example from the Paper

Here you can find a satisfiable version of the running example from our paper, where i is initialized with 0 and the following two properties are checked:

• a'[k] = a[0]
• forall 0 <= j < k. a'[j] = a[j+1]

In the formulas above, a refers to the array before execution of the loop, and a' refers to the array after execution of the loop.

Here and here, you can find unsatisfiable variants of our running examples, where the first or second of the properties above is negated, respectively. LoAT can solve all three variants in less than one second.