This page distributes the material required to reproduce the experimental results for the paper "Compositional Recurrence Analysis", FMCAD 2015.
The benchmarks and the x86_64 ELF binaries for Linear Recurrence Analysis are available in a single tarball: cra.tgz.

Tools

Binaries for all tools can be found in the bin directory. The results of running the tools can be found in the results directory. The benchmarks can be re-generated by executing
    run.sh TOOL
where TOOL is one of

Results

Legend: SAFE,UNSAFE, UNKNOWN. Times are reported in seconds.

Note that cra is a conservative static analysis, which means that it is sound for verification but not refutation. In the following table, this is reflected by the fact that cra+oct and cra never report UNSAFE, only UNKNOWN.

Safe benchmarks

Benchmarkseahorn cpachecker-1.3.10 cra+oct cra
const_true-unreach-call1.c 0.235 2.222 0.585 0.504
diamond_true-unreach-call1.c 0.572 65.856 0.638 0.560
diamond_true-unreach-call2.c 0.451 12.326 6.010 2.039
functions_true-unreach-call1.c 0.352 97.457 0.561 0.606
multivar_true-unreach-call1.c 0.276 25.298 0.588 0.524
nested_true-unreach-call1.c 0.305 82.621 0.704 0.698
overflow_true-unreach-call1.c 0.251 84.761 0.473 0.589
phases_true-unreach-call1.c 300.659 83.813 0.548 0.560
phases_true-unreach-call2.c 5.060 2.693 0.743 0.549
simple_true-unreach-call1.c 4.908 84.325 0.583 0.589
simple_true-unreach-call2.c 0.267 1.836 0.504 0.575
simple_true-unreach-call3.c 0.227 98.466 0.471 0.532
simple_true-unreach-call4.c 0.169 99.366 0.537 0.498
underapprox_true-unreach-call1.c 0.154 1.254 0.600 0.541
underapprox_true-unreach-call2.c 0.173 1.328 0.483 0.627
apache-escape-absolute_true-unreach-call.c 0.643 5.071 1.267 0.827
apache-get-tag_true-unreach-call.c 0.451 83.344 0.880 0.799
down_true-unreach-call.c 0.256 72.830 0.597 0.721
fragtest_simple_true-unreach-call.c 0.556 82.173 1.021 0.800
half_2_true-unreach-call.c 0.380 82.304 0.751 0.698
heapsort_true-unreach-call.c 0.473 81.133 3.417 3.574
id_build_true-unreach-call.c 0.443 78.954 0.781 0.629
large_const_true-unreach-call.c 0.396 2.486 1.557 0.732
MADWiFi-encode_ie_ok_true-unreach-call.c 0.278 83.579 1.620 0.615
nested6_true-unreach-call.c 0.347 103.867 1.801 0.966
nested9_true-unreach-call.c 150.224 89.704 1.392 0.950
nest-if3_true-unreach-call.c 0.360 82.686 1.413 0.800
NetBSD_loop_true-unreach-call.c 0.238 25.400 0.987 0.599
sendmail-close-angle_true-unreach-call.c 0.378 78.040 0.803 0.722
seq_true-unreach-call.c 0.257 72.795 1.242 0.675
SpamAssassin-loop_true-unreach-call.c 0.378 73.543 2.221 1.553
string_concat-noarr_true-unreach-call.c 0.226 84.609 0.816 0.719
up_true-unreach-call.c 0.208 76.891 0.741 0.656
afnp2014_true-unreach-call.c 0.234 4.042 0.575 0.556
bhmr2007_true-unreach-call.c 0.161 58.502 0.654 0.639
cggmp2005b_true-unreach-call.c 0.188 1.442 1.174 0.960
cggmp2005_true-unreach-call.c 0.177 1.244 0.495 0.496
cggmp2005_variant_true-unreach-call.c 0.158 84.831 0.614 0.558
css2003_true-unreach-call.c 0.246 2.107 0.637 0.519
ddlm2013_true-unreach-call.c 0.292 82.818 0.741 0.525
gj2007b_true-unreach-call.c 0.199 21.947 0.620 0.559
gj2007_true-unreach-call.c 300.007 1.412 0.743 0.503
gr2006_true-unreach-call.c 300.009 1.419 0.554 0.581
gsv2008_true-unreach-call.c 0.250 1.865 0.611 0.694
hhk2008_true-unreach-call.c 0.183 1.243 0.589 0.532
jm2006_true-unreach-call.c 0.196 57.478 0.475 0.589
jm2006_variant_true-unreach-call.c 0.244 24.315 0.510 0.441
count_by_1_true-unreach-call.c 0.169 84.146 0.531 0.471
count_by_1_variant_true-unreach-call.c 300.008 134.148 0.562 0.529
count_by_2_true-unreach-call.c 0.166 107.943 0.472 0.557
count_by_k_true-unreach-call.c 0.249 62.472 0.599 0.663
count_by_nondet_true-unreach-call.c 316.423 81.604 0.534 0.558
gauss_sum_true-unreach-call.c 8.899 83.757 0.620 0.630
half_true-unreach-call.c 0.326 81.024 0.825 0.600
nested_true-unreach-call.c 0.375 84.740 1.694 0.574
count_up_down_true-unreach-call_true-termination.c 0.290 81.611 0.563 0.425
for_infinite_loop_1_true-unreach-call_false-termination.c 0.148 104.979 0.562 0.431
for_infinite_loop_2_true-unreach-call_false-termination.c 2.047 75.275 0.438 0.519
heavy_false-unreach-call.c 4.615 58.701 1.876 1.410
lu.cmp_true-unreach-call.c 22.188 1.433 16.204 17.071
n.c11_true-unreach-call.c 0.342 2.575 0.677 0.607
sum01_true-unreach-call_true-termination.c 0.409 79.898 0.592 0.513
sum03_true-unreach-call_false-termination.c 0.252 80.689 0.597 0.484
sum04_true-unreach-call_true-termination.c 0.214 1.332 0.475 0.592
terminator_02_true-unreach-call_true-termination.c 0.249 2.117 0.513 0.620
terminator_03_true-unreach-call_true-termination.c 0.259 2.054 0.633 0.547
trex01_true-unreach-call.c 0.345 80.575 0.640 0.629
trex02_true-unreach-call_true-termination.c 0.365 2.036 0.559 0.501
trex03_true-unreach-call.c 0.221 2.709 2.201 0.785
trex04_true-unreach-call_false-termination.c 0.294 2.146 0.739 0.655
veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.c 0.301 57.559 1.830 13.732
while_infinite_loop_1_true-unreach-call_false-termination.c 0.164 1.335 0.460 0.463
while_infinite_loop_2_true-unreach-call_false-termination.c 0.328 1.317 0.499 0.452
while_infinite_loop_3_true-unreach-call_false-termination.c 0.232 1.263 0.461 0.469
count_by_nondet-symbolic.c 159.851 89.375 0.751 0.542
divides.c 88.636 10.688 5.616 5.710
mult.c 0.239 84.414 0.554 0.489
mult_commute.c 0.278 2.177 0.688 0.444
nested-symbolic.c 100.020 83.992 1.974 0.739
qr.c 0.219 86.047 0.588 0.611
qr-nested.c 305.683 82.483 0.999 0.764
quotient.c 300.076 85.419 0.585 0.607

Unsafe benchmarks

Benchmarkseahorn cpachecker-1.3.10 cra+oct cra
const_false-unreach-call1.c 25.514 6.638 0.703 0.541
diamond_false-unreach-call1.c 0.606 4.539 0.671 0.555
functions_false-unreach-call1.c 300.008 112.034 0.584 0.528
multivar_false-unreach-call1.c 0.244 2.266 0.655 0.517
nested_false-unreach-call1.c 0.292 83.395 0.631 0.527
phases_false-unreach-call1.c 300.190 83.707 0.651 0.456
phases_false-unreach-call2.c 2.153 1.602 0.734 0.506
simple_false-unreach-call1.c 301.668 84.302 0.524 0.586
simple_false-unreach-call2.c 6.536 1.458 0.542 0.570
simple_false-unreach-call3.c 1.832 1.470 0.591 0.486
simple_false-unreach-call4.c 309.781 84.303 0.611 0.598
underapprox_false-unreach-call1.c 0.408 2.055 0.653 0.557
underapprox_false-unreach-call2.c 0.434 1.666 0.681 0.502
id_trans_false-unreach-call.c 0.214 3.091 0.609 0.671
gcnr2008_false-unreach-call.c 0.230 65.002 1.150 0.999
heavy_true-unreach-call.c 322.827 83.306 1.872 1.412
ludcmp_false-unreach-call.c 0.514 88.178 12.731 27.250
nec11_false-unreach-call.c 0.272 27.861 0.694 0.626
nec20_false-unreach-call.c 0.223 1.940 0.911 0.550
terminator_01_false-unreach-call_false-termination.c 0.362 1.551 0.505 0.479
terminator_02_false-unreach-call_true-termination.c 0.280 1.578 0.713 0.603
terminator_03_false-unreach-call_true-termination.c 0.263 2.208 0.644 0.580
verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.c 0.467 1.963 76.722 68.142
count_up_down_false-unreach-call_true-termination.c 0.379 1.670 0.643 0.534
for_bounded_loop1_false-unreach-call_true-termination.c 0.349 3.283 0.632 0.638
sum01_bug02_false-unreach-call_true-termination.c 0.258 6.000 0.796 0.578
sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.c 0.284 3.139 0.640 0.494
sum01_false-unreach-call_true-termination.c 0.376 4.006 0.630 0.460
sum03_false-unreach-call_true-termination.c 0.353 1.859 0.731 0.599
sum04_false-unreach-call_true-termination.c 0.338 1.676 0.680 0.623
trex01_false-unreach-call_true-termination.c 0.621 1.569 0.760 0.662
trex02_false-unreach-call_true-termination.c 0.374 1.830 0.573 0.579
trex03_false-unreach-call_true-termination.c 0.289 2.287 2.215 0.741
while_infinite_loop_4_false-unreach-call_true-termination.c 0.222 1.482 0.474 0.431
divides_err.c 292.161 1.485 0.616 0.605
mult_err.c 2.704 1.975 0.478 0.610
qr-nested_err.c 0.315 3.149 1.003 0.623
quotient_err.c 0.295 1.481 0.643 0.546