Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following GIT repository: (for SV-COMP 2020 visit the tag 'svcomp20'): 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/*.yml array-industry-pattern/*.yml reducercommutativity/*.yml array-tiling/*.yml array-programs/*.yml array-crafted/*.yml array-multidimensional/*.yml array-patterns/*.yml array-cav19/*.yml array-lopstr16/*.yml array-fpi/*.yml
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/*.yml bitvector-regression/*.yml bitvector-loops/*.yml
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/*.yml ssh-simplified/*.yml locks/*.yml ntdrivers/*.yml ssh/*.yml
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/*.yml eca-rers2018/*.yml psyco/*.yml eca-programs/*.yml
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/*.yml floats-cbmc-regression/*.yml float-benchs/*.yml floats-esbmc-regression/*.yml float-newlib/*.yml loop-floats-scientific-comp/*.yml
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/*.yml list-properties/*.yml ldv-regression/*.yml ddv-machzwd/*.yml forester-heap/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml list-simple/*.yml heap-data/*.yml list-ext3-properties/*.yml
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/*.yml loop-acceleration/*.yml loop-crafted/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml loop-industry-pattern/*.yml loops-crafted-1/*.yml loop-invariants/*.yml loop-simple/*.yml verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/tree_del_iter.yml verifythis/tree_del_iter_incorrect.yml nla-digbench/*.yml
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/*.yml
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/*.yml recursive-simple/*.yml recursive-with-pointer/*.yml verifythis/tree_del_rec.yml verifythis/tree_del_rec_incorrect.yml verifythis/tree_max.yml verifythis/tree_max_incorrect.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
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/*.yml seq-mthreaded/*.yml seq-mthreaded-reduced/*.yml seq-pthread/*.yml
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
Contains tasks for checking memory safety of array-based programs.
The verification tasks consist of the programs that match
array-memsafety/*.yml array-examples/*.yml array-memsafety-realloc/*.yml verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
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: 32 bit
MemSafety-Heap
Contains tasks for checking memory safety of programs.
The verification tasks consist of the programs that match
memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml list-ext-properties/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
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: 32 bit
MemSafety-LinkedLists
Contains tasks for checking memory safety of programs.
The verification tasks consist of the programs that match
heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml ddv-machzwd/*.yml list-simple/*.yml list-ext3-properties/*.yml
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: 32 bit
MemSafety-Other
Contains tasks for checking memory safety of programs.
The verification tasks consist of the programs that match
loops/*.yml loop-acceleration/*.yml ntdrivers/*.yml ntdrivers-simplified/*.yml locks/*.yml memsafety-ext3/*.yml pthread-memsafety/*.yml memsafety-bftpd/*.yml
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: 32 bit
MemSafety-TerminCrafted
Contains tasks for checking memory safety of array-based programs.
The verification tasks consist of the programs that match
termination-crafted/*.yml
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
MemSafety-MemCleanup
Contains tasks for checking memory safety of programs.
The verification tasks consist of the programs that match
list-ext-properties/*.yml heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml list-ext3-properties/*.yml memsafety-bftpd/*.yml verifythis/tree_max.yml verifythis/tree_del_iter.yml verifythis/tree_del_rec.yml
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/*.yml pthread-atomic/*.yml pthread-ext/*.yml pthread-wmm/*.yml pthread-lit/*.yml ldv-races/*.yml ldv-linux-3.14-races/*.yml pthread-complex/*.yml pthread-driver-races/*.yml pthread-C-DAC/*.yml pthread-divine/*.yml pthread-nondet/*.yml
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/*.yml termination-crafted/*.yml termination-crafted-lit/*.yml termination-numeric/*.yml
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/*.yml recursive-simple/*.yml bitvector/*.yml psyco/*.yml
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/*.yml termination-crafted-lit/*.yml termination-numeric/*.yml termination-restricted-15/*.yml
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/*.yml termination-memory-alloca/*.yml termination-memory-linkedlists/*.yml termination-15/*.yml termination-recursive-malloc/*.yml
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
array-examples/*.yml array-industry-pattern/*.yml bitvector/*.yml bitvector-regression/*.yml bitvector-loops/*.yml ntdrivers-simplified/*.yml ssh-simplified/*.yml locks/*.yml ntdrivers/*.yml eca-rers2012/*.yml psyco/*.yml floats-cdfpl/*.yml floats-cbmc-regression/*.yml ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml loops/*.yml loop-acceleration/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml product-lines/*.yml recursive/*.yml recursive-simple/*.yml systemc/*.yml seq-mthreaded/*.yml seq-pthread/*.yml reducercommutativity/*.yml array-memsafety/*.yml memsafety/*.yml memsafety-ext/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml pthread-atomic/*.yml
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.
SoftwareSystems-AWS-C-Common-ReachSafety
Contains programs from the AWS C commons library
The verification tasks consist of the programs that match
aws-c-common/*.yml
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 64 bit
SoftwareSystems-BusyBox-MemSafety
Contains problems from the software system BusyBox.
The verification tasks consist of the programs that match
busybox-1.22.0/*.yml
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
SoftwareSystems-BusyBox-NoOverflows
Contains problems from the software system BusyBox.
The verification tasks consist of the programs that match
busybox-1.22.0/*.yml
with the specification
CHECK( init(main()), LTL(G ! overflow) )
and the following parameter:
Architecture: 64 bit
SoftwareSystems-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/*.yml ldv-linux-3.4-simple/*.yml ldv-linux-3.7.3/*.yml ldv-commit-tester/*.yml ldv-consumption/*.yml ldv-linux-3.12-rc1/*.yml ldv-linux-3.16-rc1/*.yml ldv-validator-v0.6/*.yml ldv-validator-v0.8/*.yml ldv-linux-4.2-rc1/*.yml ldv-linux-3.14/*.yml ldv-challenges/*.yml ldv-linux-4.0-rc1-mav/*.yml
with the specification
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
and the following parameter:
Architecture: 64 bit
SoftwareSystems-OpenBSD-MemSafety
Contains problems that require the analysis of memory safety.
The verification tasks consist of the programs that match
openbsd-6.2/*.yml
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
SoftwareSystems-SQLite-MemSafety
Contains problems from the software SQLite
The verification tasks consist of the programs that match
sqlite/*.yml
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
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-Java
The verification tasks consist of the programs that match
jayhorn-recursive/*.yml jbmc-regression/*.yml jpf-regression/*.yml java-ranger-regression/*.yml java-ranger-regression/WBS/*.yml MinePump/*.yml algorithms/*.yml
with the specification
CHECK( init(Main.main()), LTL(G assert) )
and the following parameter:
Architecture: --