Benchmark Verification Tasks

All verification tasks are available for web browsing and for download via the following GIT repository: (for SV-COMP 2024 visit the tag 'svcomp24'): 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 (2024) 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/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
array-memsafety/*.yml
array-memsafety-realloc/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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/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
memory-model/*.yml
unsignedintegeroverflow-sas23/*.yml
longjmp/*.yml
signedintegeroverflow-regression/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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/Floats

Contains tasks for checking programs with floating-point arithmetics. Contains programs from the Plain C Neural Network Verification Benchmark

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

neural-networks/*.yml

floats-nonlinear/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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

ldv-regression/*.yml
list-ext-properties/*.yml
list-ext2-properties/*.yml
ldv-sets/*.yml
heap-data/*.yml
memsafety/*.yml
memsafety-ext/*.yml
memsafety-ext2/*.yml
memsafety-ext3/*.yml
memsafety-bftpd/*.yml
memory-alloca/*.yml
ldv-memsafety/*.yml
ldv-memsafety-bitfields/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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-invariants64/*.yml
loop-simple/*.yml
loop-zilu/*.yml
nla-digbench/*.yml
nla-digbench-scaling/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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/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
recursified_loop-crafted/*.yml
recursified_loop-invariants/*.yml
recursified_loop-simple/*.yml
recursified_nla-digbench/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/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/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/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())) )

c/Hardware

Contains programs translated by Btor2C from word-level hardware-verification tasks.

The verification tasks consist of the programs that match

hardware-verification-array/btor2c-lazyMod.*.yml
hardware-verification-bv/btor2c-lazyMod.*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/Hardness

Contains various tasks which require a wide variety of techniques in order to determine reachability. Some make specific use of pointers, some of arrays, some of structs, some of floats, and some combine everything. These examples are derived from the NFM2022 paper "Configurable Benchmarks for C Model Checkers" (https://doi.org/10.1007/978-3-031-06773-0_18) Artifact: https://doi.org/10.5281/zenodo.6392205

The verification tasks consist of the programs that match

hardness-nfm22/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/Fuzzle

Contains tasks from the Fuzzle tool benchmark set.

The verification tasks consist of the programs that match

fuzzle-programs/*.yml

with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

2. MemSafety

This category consists of the following sub-categories.

c/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
array-memsafety/*.yml
array-memsafety-realloc/*.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/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

ldv-regression/*.yml
list-ext-properties/*.yml
list-ext2-properties/*.yml
ldv-sets/*.yml
heap-data/*.yml
memsafety/*.yml
memsafety-ext/*.yml
memsafety-ext2/*.yml
memsafety-ext3/*.yml
memsafety-bftpd/*.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/LinkedLists

Contains tasks for checking memory safety of programs.

The verification tasks consist of the programs that match

memsafety-broom/*.yml
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/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) )

c/MemSafety-Juliet

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) )

c/MemSafety-MemCleanup

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G valid-memcleanup) )

3. ConcurrencySafety

This category consists of the following sub-categories.

c/ConcurrencySafety-Main

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/ConcurrencySafety-MemSafety

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) )

c/ConcurrencySafety-NoOverflows

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

c/NoDataRace-Main

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! data-race) )

4. NoOverflows

This category consists of the following sub-categories.

c/NoOverflows-Main

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

c/NoOverflows-Juliet

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

5. Termination

This category consists of the following sub-categories.

c/Termination-BitVectors

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(F end) )

c/Termination-MainControlFlow

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(F end) )

c/Termination-MainHeap

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(F end) )

c/Termination-Other

The verification tasks consist of the programs that match


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

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/SoftwareSystems-coreutils-MemSafety

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) )

c/SoftwareSystems-coreutils-NoOverflows

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

c/SoftwareSystems-BusyBox-NoOverflows

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

c/SoftwareSystems-DeviceDriversLinux64-ReachSafety

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/SoftwareSystems-DeviceDriversLinux64Large-ReachSafety

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/SoftwareSystems-DeviceDriversLinux64-MemSafety

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) )

c/SoftwareSystems-Other-ReachSafety

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/SoftwareSystems-Other-MemSafety

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) )

c/SoftwareSystems-uthash-ReachSafety

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! call(reach_error())) )

c/SoftwareSystems-uthash-MemSafety

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) )

c/SoftwareSystems-uthash-NoOverflows

The verification tasks consist of the programs that match


with the specification:

CHECK( init(main()), LTL(G ! overflow) )

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
float-nonlinear-calculation/*.yml

with the specification:

CHECK( init(Main.main()), LTL(G assert) )