Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following GIT repository: (for SV-COMP 2022 visit the tag 'svcomp22'): 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.
The authorative definition of the category structure is maintained in the repository for the benchmark definitions (https://gitlab.com/sosy-lab/sv-comp/bench-defs).
1. ReachSafety
This category consists of the following sub-categories.
c/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(reach_error())) )
c/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(reach_error())) )
c/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 openssl-simplified/*.yml locks/*.yml ntdrivers/*.yml openssl/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
c/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(reach_error())) )
c/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(reach_error())) )
c/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(reach_error())) )
c/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 loop-zilu/*.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 nla-digbench-scaling/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
c/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(reach_error())) )
c/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/prefixsum_rec.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(reach_error())) )
c/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(reach_error())) )
c/ReachSafety-XCSP
Contains tasks from the XCSP_to_C tool benchmark set.
The verification tasks consist of the programs that match
xcsp/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
c/ReachSafety-Combinations
Contains programs combined from other sv-benchmark tasks through loose coupling
The verification tasks consist of the programs that match
combinations/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
2. MemSafety
This category consists of the following sub-categories.
c/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 termination-crafted/Arrays*.yml termination-crafted/LexIndexValue*.yml termination-crafted/NonTermination3-1.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) )
c/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) )
c/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) )
c/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 termination-crafted/4BitCounterPointer.yml termination-crafted/SyntaxSupportPointer*.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) )
c/MemSafety-Juliet
Contains tasks for checking memory safety of programs from Juliet Test Suite. CWE415_Double_Free CWE476_NULL_Pointer_Dereference CWE121_Stack_Based_Buffer_Overflow CWE401_Memory_Leak CWE590_Free_Memory_Not_on_Heap
The verification tasks consist of the programs that match
Juliet_Test/CWE415*.yml Juliet_Test/CWE476*_int*.yml Juliet_Test/CWE476*_long*.yml Juliet_Test/CWE476*_struct*.yml Juliet_Test/CWE121*rand*.yml Juliet_Test/CWE121*fgets*.yml Juliet_Test/CWE121*large*.yml Juliet_Test/CWE401*__int*.yml Juliet_Test/CWE401*__struct*.yml Juliet_Test/CWE401*__twoIntsStruct*.yml Juliet_Test/CWE590*.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) )
c/MemSafety-MemCleanup
Contains tasks for checking memory safety of programs. Should be kept in sync with MemSafety-Juliet.set because we do not use all Juliet tasks yet.
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/*.yml memsafety-bftpd/*.yml verifythis/tree_max.yml verifythis/tree_del_iter.yml verifythis/tree_del_rec.yml Juliet_Test/CWE415*.yml Juliet_Test/CWE476*_int*.yml Juliet_Test/CWE476*_long*.yml Juliet_Test/CWE476*_struct*.yml Juliet_Test/CWE121*rand*.yml Juliet_Test/CWE121*fgets*.yml Juliet_Test/CWE121*large*.yml Juliet_Test/CWE401*__int*.yml Juliet_Test/CWE401*__struct*.yml Juliet_Test/CWE401*__twoIntsStruct*.yml Juliet_Test/CWE590*.yml
with the specification:
CHECK( init(main()), LTL(G valid-memcleanup) )
3. ConcurrencySafety
This category consists of the following sub-categories.
c/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 goblint-regression/*.yml weaver/*.yml pthread-deagle/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
4. NoOverflows
This category consists of the following sub-categories.
c/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) )
c/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 loop-zilu/*.yml goblint-regression/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
5. Termination
This category consists of the following sub-categories.
c/Termination-BitVectors
Contains programs for which termination should be decided.
The verification tasks consist of the programs that match
termination-bwb/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
c/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 termination-nla/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
c/Termination-MainHeap
Contains programs for which termination should be decided.
The verification tasks consist of the programs that match
termination-dietlibc/*.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) )
c/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 openssl-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 uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
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.
c/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(reach_error())) )
c/SoftwareSystems-BusyBox-ReachSafety
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 ! call(reach_error())) )
c/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) )
c/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) )
c/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(reach_error())) )
c/SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
Contains large tasks from the DeviceDrivers64 category (from the LDV project).
The verification tasks consist of the programs that match
ldv-challenges/linux-3.14_complex_emg_linux-alloc-spinlock_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-kernel-locking-mutex_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-usb-dev_drivers-net-ethernet-sfc-sfc.cil.yml ldv-linux-3.14/linux-3.14_complex_emg_linux-drivers-clk1_drivers-net-ethernet-sfc-sfc.cil.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--gpu--drm--amd--amdgpu--amdgpu.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--gpu--drm--i915--i915.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--i915--i915.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
c/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) )
c/SoftwareSystems-uthash-MemSafety
Contains problems from the uthash hashing library.
The verification tasks consist of the programs that match
uthash-2.0.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) )
c/SoftwareSystems-uthash-NoOverflows
Contains problems from the uthash hashing library.
The verification tasks consist of the programs that match
uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
c/SoftwareSystems-uthash-ReachSafety
Contains problems from the uthash hashing library.
The verification tasks consist of the programs that match
uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
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.
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 java-ranger-regression/alarm/*.yml java-ranger-regression/infusion/*.yml java-ranger-regression/siena_eqchk/*.yml java-ranger-regression/replace5_eqchk/*.yml java-ranger-regression/nanoxml_eqchk/*.yml java-ranger-regression/printtokens_eqchk/*.yml MinePump/*.yml algorithms/*.yml juliet-java/*.yml jdart-regression/*.yml securibench/*.yml
with the specification:
CHECK( init(Main.main()), LTL(G assert) )