Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following GIT repository: (for SV-COMP 2019 visit the tag 'svcomp19'): https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
This edition of the competition on software verification is based on the following categories of verification tasks.
The verification tasks were contributed by several research and development groups.
After the submission deadline for verification tasks, a group of people (organizer and participants)
were working on improving the quality of the verification tasks.
That means that after the sets were made public,
some programs were removed (not qualified, no property encoded, unknown architecture),
and some programs got technically improved (CIL simplifications, compiler warnings, memory model).
These changes have improved the overall quality of the final set of programs for the competition,
and have not changed the intended verification result;
all changes are tracked in the public repository.
Thanks to all participants that contributed programs, sent patches, and commented on the sets.
As announced in the rules and definitions, the verification tasks are not necessarily preprocessed with CIL (which was a restriction for the first SV-COMP). For each category, we specify whether its verification tasks assume a 32-bit or a 64-bit architecture.
For illustration, a structured overview shows the categories. Rankings will be provided for the first- and second-level categories, and Falsification, which is not shown in the figure.
1. ReachSafety
This category consists of the following sub-categories.
ReachSafety-Arrays
Contains tasks for which treatment of arrays is necessary in order to determine reachability.
The verification tasks consist of the programs that match
array-examples/*_false-unreach-call*.i array-examples/*_true-unreach-call*.i array-examples/*_true-unreach-call*-reducer.c array-industry-pattern/*_false-unreach-call*.i array-industry-pattern/*_true-unreach-call*.i reducercommutativity/*_false-unreach-call*.i reducercommutativity/*_true-unreach-call*.i array-tiling/*_false-unreach-call*.i array-tiling/*_true-unreach-call*.i array-programs/*_false-unreach-call*.i array-programs/*_true-unreach-call*.i array-crafted/*_true-unreach-call*.i array-crafted/zero_sum*_true-unreach-call*.c array-multidimensional/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-BitVectors
Contains tasks for which treatment of bit-operations is necessary.
The verification tasks consist of the programs that match
bitvector/*_false-unreach-call*.i bitvector/*_true-unreach-call*.i bitvector/*_false-unreach-call*.BV.c.cil.c bitvector/*_true-unreach-call*.c.cil.c bitvector-regression/*_false-unreach-call*.c bitvector-regression/*_true-unreach-call*.c bitvector-loops/*_false-unreach-call*.i # bitvector-loops/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-ControlFlow
Contains programs for which the correctness depends mostly on the control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency.
The verification tasks consist of the programs that match
ntdrivers-simplified/*_false-unreach-call*.cil.c ntdrivers-simplified/*_true-unreach-call*.cil.c ssh-simplified/*_false-unreach-call*.cil.c ssh-simplified/*_true-unreach-call*.cil.c locks/*_false-unreach-call*.c locks/*_true-unreach-call*.c ntdrivers/*_false-unreach-call*.i.cil.c ntdrivers/*_true-unreach-call*.i.cil.c ssh/*_false-unreach-call*.i.cil.c ssh/*_true-unreach-call*.i.cil.c
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-ECA
Contains programs that represent event-condition-action systems.
The verification tasks consist of the programs that match
eca-rers2012/*_false-unreach-call*.c eca-rers2012/*_true-unreach-call*.c psyco/*_false-unreach-call*.c psyco/*_true-unreach-call*.c eca-programs/*_false-unreach-call*.c eca-programs/*_true-unreach-call*.c
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Floats
Contains tasks for checking programs with floating-point arithmetics.
The verification tasks consist of the programs that match
floats-cdfpl/*_false-unreach-call*.i floats-cdfpl/*_true-unreach-call*.i floats-cbmc-regression/*_true-unreach-call*.i float-benchs/*_false-unreach-call*.c float-benchs/*_true-unreach-call*.c floats-esbmc-regression/*_true-unreach-call*.i floats-esbmc-regression/*_false-unreach-call*.i floats-esbmc-regression/*_true-unreach-call*-reducer.c floats-esbmc-regression/*_false-unreach-call*-reducer.c float-newlib/*true-unreach-call*.c float-newlib/*false-unreach-call*.c loop-floats-scientific-comp/*_true-unreach-call*.i loop-floats-scientific-comp/*_false-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Heap
Contains tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.
The verification tasks consist of the programs that match
heap-manipulation/*_false-unreach-call*.i heap-manipulation/*_true-unreach-call*.i list-properties/*_false-unreach-call*.i list-properties/*_true-unreach-call*.i ldv-regression/*_false-unreach-call*.i ldv-regression/*_true-unreach-call*.i ldv-regression/test[0-9][0-9]_false-unreach-call*.c ldv-regression/test[0-9][0-9]_true-unreach-call*.c ddv-machzwd/*_false-unreach-call*.i ddv-machzwd/*_true-unreach-call*.i forester-heap/*_false-unreach-call*.i forester-heap/*_true-unreach-call*.i list-ext-properties/*_false-unreach-call*.i list-ext2-properties/*-unreach-call*.i ldv-sets/*_false-unreach-call*.i ldv-sets/*_true-unreach-call*.i list-simple/*_true-unreach-call*.i heap-data/*_true-unreach-call*.i list-ext3-properties/*_false-unreach-call*.i list-ext3-properties/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Loops
Contains tasks for which loop analysis is necessary.
The verification tasks consist of the programs that match
loops/*_false-unreach-call*.i loops/*_true-unreach-call*.i loop-acceleration/*_false-unreach-call*.i loop-acceleration/*_true-unreach-call*.i loop-crafted/*_false-unreach-call*.i loop-crafted/*_true-unreach-call*.i loop-crafted/*_true-unreach-call*-reducer.c loop-invgen/*_false-unreach-call*.i loop-invgen/*_true-unreach-call*.i loop-invgen/*_true-unreach-call*-reducer.c loop-lit/*_true-unreach-call*.i loop-lit/*_false-unreach-call*.i loop-lit/*_true-unreach-call*-reducer.c loop-new/*_true-unreach-call*.i loop-new/*_true-unreach-call*-reducer.c loop-industry-pattern/*_true-unreach-call*.c loops/heavy_true-unreach-call.c loops/compact_false-unreach-call.c loops/heavy_false-unreach-call.c loops-crafted-1/*_false-unreach-call*.c loops-crafted-1/*_true-unreach-call*.c loop-invariants/*_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-ProductLines
Contains programs that represents 'products' and 'product simulators' that are derived using different configurations of product lines.
The verification tasks consist of the programs that match
product-lines/elevator*_false-unreach-call*.c product-lines/elevator*_true-unreach-call*.c product-lines/email*_false-unreach-call*.c product-lines/email*_true-unreach-call*.c product-lines/minepump*_false-unreach-call*.c product-lines/minepump*_true-unreach-call*.c
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Recursive
Contains tasks for which recursive analysis is necessary.
The verification tasks consist of the programs that match
recursive/*_false-unreach-call*.c recursive/*_true-unreach-call*.c recursive-simple/*_false-unreach-call*.c recursive-simple/*_true-unreach-call*.c
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
ReachSafety-Sequentialized
Contains sequentialized concurrent programs that were derived from SystemC programs. The programs were transformed to pure C programs by incorporating the scheduler into the C code.
The verification tasks consist of the programs that match
systemc/*_false-unreach-call*.cil.c systemc/*_true-unreach-call*.cil.c seq-mthreaded/*_false-unreach-call.*.c seq-mthreaded/*_true-unreach-call.*.c seq-mthreaded-reduced/*_false-unreach-call*-reducer.c seq-mthreaded-reduced/*_true-unreach-call*-reducer.c seq-pthread/*_false-unreach-call*.i seq-pthread/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
2. MemSafety
This category consists of the following sub-categories.
MemSafety-Arrays
The verification tasks consist of the programs that match
with the specification
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
and the following parameter:
Architecture:
MemSafety-Heap
The verification tasks consist of the programs that match
with the specification
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
and the following parameter:
Architecture:
MemSafety-LinkedLists
The verification tasks consist of the programs that match
with the specification
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
and the following parameter:
Architecture:
MemSafety-Other
The verification tasks consist of the programs that match
with the specification
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
and the following parameter:
Architecture:
MemSafety-MemCleanup
Contains tasks for checking memory safety of programs.
The verification tasks consist of the programs that match
list-ext-properties/*_false-valid-memcleanup*.i heap-manipulation/*_false-valid-memcleanup*.i forester-heap/*_false-valid-memcleanup*.i list-properties/*_false-valid-memcleanup*.i list-ext3-properties/*_false-valid-memcleanup*.i
with the specification
CHECK( init(main()), LTL(G valid-memcleanup) )
and the following parameter:
Architecture: 32 bit
3. ConcurrencySafety
This category consists of the following sub-categories.
ConcurrencySafety-Main
Contains concurrency problems.
The verification tasks consist of the programs that match
pthread/*_false-unreach-call*.i pthread/*_true-unreach-call*.i pthread-atomic/*_false-unreach-call*.i pthread-atomic/*_true-unreach-call*.i pthread-ext/*_false-unreach-call*.i pthread-ext/*_true-unreach-call*.i pthread-wmm/*_false-unreach-call*.i pthread-wmm/*_true-unreach-call*.i pthread-lit/*_false-unreach-call*.i pthread-lit/*_true-unreach-call*.i ldv-races/*_true-unreach-call*.i ldv-races/*_false-unreach-call*.i ldv-linux-3.14-races/*_false-unreach-call*.i ldv-linux-3.14-races/*_true-unreach-call*.i pthread-complex/*_false-unreach-call*.i pthread-complex/*_true-unreach-call*.i pthread-driver-races/*_true-unreach-call*.i pthread-driver-races/*_false-unreach-call*.i pthread-C-DAC/*_true-unreach-call*.i pthread-C-DAC/*_false-unreach-call*.i pthread-divine/*_false-unreach-call*.i pthread-divine/*_true-unreach-call*.i pthread-nondet/*_false-unreach-call*.i pthread-nondet/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 32 bit
4. NoOverflows
This category consists of the following sub-categories.
NoOverflows-BitVectors
Contains tasks for checking if variables of type signed integers overflow.
The verification tasks consist of the programs that match
signedintegeroverflow-regression/*_false-no-overflow*.c.i signedintegeroverflow-regression/*_true-no-overflow*.c.i termination-crafted/*_false-no-overflow*.c termination-crafted/*_true-no-overflow*.c termination-crafted-lit/*_false-no-overflow*.c termination-crafted-lit/*_true-no-overflow*.c termination-numeric/*_false-no-overflow*.c termination-numeric/*_true-no-overflow*.c
with the specification
CHECK( init(main()), LTL(G ! overflow) )
and the following parameter:
Architecture: 64 bit
NoOverflows-Other
Contains tasks for checking if variables of type signed integers overflow.
The verification tasks consist of the programs that match
recursive/*_false-no-overflow*.c recursive/*_true-no-overflow*.c recursive-simple/*_false-no-overflow*.c recursive-simple/*_true-no-overflow*.c bitvector/*_false-no-overflow*.i bitvector/*_true-no-overflow*.i psyco/*_false-no-overflow*.c
with the specification
CHECK( init(main()), LTL(G ! overflow) )
and the following parameter:
Architecture: 32 bit
5. Termination
This category consists of the following sub-categories.
Termination-MainControlFlow
Contains programs for which termination should be decided.
The verification tasks consist of the programs that match
termination-crafted/*_false-termination*.c termination-crafted/*_true-termination*.c termination-crafted-lit/*_false-termination*.c termination-crafted-lit/*_true-termination*.c termination-numeric/*_true-termination*.c termination-restricted-15/*_true-termination*.c termination-restricted-15/*_false-termination*.c
with the specification
CHECK( init(main()), LTL(F end) )
and the following parameter:
Architecture: 64 bit
Termination-MainHeap
Contains programs for which termination should be decided.
The verification tasks consist of the programs that match
termination-libowfat/*_true-termination*.c.i termination-memory-alloca/*_false-termination*.c.i termination-memory-alloca/*_true-termination*.c.i termination-memory-linkedlists/*_false-termination*.c.i termination-memory-linkedlists/*_true-termination*.c.i termination-15/*_true-termination*.c.i termination-15/*_false-termination*.c.i termination-recursive-malloc/*_true-termination*.c.i
with the specification
CHECK( init(main()), LTL(F end) )
and the following parameter:
Architecture: 64 bit
Termination-Other
Contains programs for which termination should be decided.
The verification tasks consist of the programs that match
# from ReachSafety-Arrays array-examples/*_true-termination*.i array-industry-pattern/*_true-termination*.i # from ReachSafety-BitVectors bitvector/*_false-termination*.i bitvector/*_true-termination*.i bitvector/*_false-termination*.BV.c.cil.c bitvector/*_true-termination*.c.cil.c bitvector-regression/*_true-termination*.c bitvector-loops/*_true-termination*.i # from ReachSafety-ControlFlow ntdrivers-simplified/*_true-termination*.cil.c ssh-simplified/*_false-termination*.cil.c ssh-simplified/*_true-termination*.cil.c locks/*_false-termination*.c ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c ntdrivers/*_true-termination*.i.cil.c # from ReachSafety-ECA eca-rers2012/*_false-termination*.c psyco/*_false-termination.c # from ReachSafety-Floats floats-cdfpl/*_true-termination*.i floats-cbmc-regression/*_true-termination*.i # from ReachSafety-Heap ldv-regression/*_true-termination*.i ldv-regression/*_false-termination*.i ldv-regression/test[0-9][0-9]*_true-termination*.c list-ext-properties/*_true-termination*.i list-ext2-properties/*_false-termination*.i ldv-sets/*_true-termination*.i # from ReachSafety-Loops loops/*_false-termination*.i loops/*_true-termination*.i loop-acceleration/*_true-termination*.i loop-acceleration/*_false-termination*.i loop-invgen/*_false-termination*.i loop-invgen/*_true-termination*.i loop-lit/*_true-termination*.i loop-lit/*_false-termination*.i loop-new/*_true-termination*.i # from ReachSafety-ProductLines product-lines/*_true-termination*.c product-lines/*_false-termination*.c # from ReachSafety-Recursive recursive/*_false-termination*.c recursive/*_true-termination*.c recursive-simple/*_true-termination*.c # from ReachSafety-Sequentialized systemc/*_false-termination*.cil.c seq-mthreaded/*_true-termination*.c seq-pthread/*_true-termination*.i # from ReachSafety-Arrays reducercommutativity/*_true-termination*.i # from MemSafety-Arrays array-memsafety/*_true-termination*.i # from MemSafety-Heap memsafety/*_true-termination*.i memsafety/*_false-termination*.i memsafety-ext/*_false-termination*.i ldv-memsafety/*_true-termination*.c ldv-memsafety/*_true-termination*.i ldv-memsafety-bitfields/*_true-termination*.i # from Concurrency pthread-atomic/*_true-termination*.i # from NoOverflows-BitVectors # is 64bit and needs own category # signedintegeroverflow-regression/*true-termination*.c.i
with the specification
CHECK( init(main()), LTL(F end) )
and the following parameter:
Architecture: 32 bit
6. SoftwareSystems
This category consists of several sets of verification tasks. Each of these sets is an own sub-category. While the categories above are collections of rather `academic', or synthesized, example verification tasks, this category aims to represent verification tasks from real software systems.
Systems_BusyBox_MemSafety
Contains problems from the software system BusyBox.
The verification tasks consist of the programs that match
busybox-1.22.0/*_false-valid-deref*.i #busybox-1.22.0/*_false-valid-free*.i busybox-1.22.0/*_false-valid-memtrack*.i busybox-1.22.0/*_true-valid-memsafety*.i
with the specification
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
and the following parameter:
Architecture: 64 bit
Systems_BusyBox_NoOverflows
Contains problems from the software system BusyBox.
The verification tasks consist of the programs that match
busybox-1.22.0/*_false-no-overflow*.i busybox-1.22.0/*_true-no-overflow*.i
with the specification
CHECK( init(main()), LTL(G ! overflow) )
and the following parameter:
Architecture: 64 bit
Systems_DeviceDriversLinux64_ReachSafety
Contains problems that require the analysis of pointer aliases and function pointers.
The verification tasks consist of the programs that match
ldv-linux-3.0/*_false-unreach-call*.i ldv-linux-3.0/*_true-unreach-call*.i ldv-linux-3.4-simple/*_false-unreach-call*.i ldv-linux-3.4-simple/*_true-unreach-call*.i ldv-linux-3.7.3/*_false-unreach-call*.i ldv-linux-3.7.3/*_true-unreach-call*.i ldv-commit-tester/*_false-unreach-call*.i ldv-commit-tester/*_true-unreach-call*.i ldv-consumption/*_false-unreach-call*.i ldv-consumption/*_true-unreach-call*.i ldv-linux-3.12-rc1/*_false-unreach-call*.i ldv-linux-3.12-rc1/*_true-unreach-call*.i ldv-linux-3.16-rc1/*_false-unreach-call*.i ldv-linux-3.16-rc1/*_true-unreach-call*.i ldv-validator-v0.6/*_false-unreach-call*.i ldv-validator-v0.8/*_false-unreach-call*.i ldv-linux-4.2-rc1/*_false-unreach-call*.i ldv-linux-4.2-rc1/*_true-unreach-call*.i ldv-linux-3.14/*_false-unreach-call*.i ldv-linux-3.14/*_true-unreach-call*.i ldv-challenges/*_false-unreach-call*.i ldv-challenges/*_true-unreach-call*.i ldv-linux-4.0-rc1-mav/*_false-unreach-call*.i ldv-linux-4.0-rc1-mav/*_true-unreach-call*.i
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 64 bit
7. C-Overall
The category Overall contains all verification tasks of all above categories. Each above-mentioned main category is an own sub-category in category Overall. (The weighting schema is explained on the rules page.)
8. C-Falsification
The category Falsification consists of all verification tasks with safety properties and the results "correct TRUE" and "incorrect TRUE" are not counted. (The weighting schema is the same as for Overall.)
9. Java-Overall
The category consists of one category that contains a set of verification tasks in Java.
ReachSafety
The verification tasks consist of the programs that match
jayhorn-recursive/*.yml jbmc-regression/*.yml jpf-regression/*.yml MinePump/*.yml
with the specification
CHECK( init(Main.main()), LTL(G assert) )
and the following parameter:
Architecture: --