Benchmark Verification Tasks

All verification tasks are available for web browsing and for download via the following SVN repository: https://github.com/dbeyer/sv-benchmarks/releases/tag/svcomp13

The 2013 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). In several categories, we just added the C files as they were before CIL preprocessing.

1. Bit Vectors

The set BitVectors contains verification tasks for which treatment of bit-operations is necessary:

bitvector/*_unsafe.i
bitvector/*_safe.i
bitvector/*_unsafe.BV.c.cil.c
bitvector/*_safe.BV.c.cil.c
bitvector/*_safe.c.cil.c

The benchmark set was provided by the Kratos project.
Description: bitvector

2. Concurrency

Some concurrency problems are contained in the set Concurrency:

pthread/*_unsafe.cil.c
pthread/*_unsafe.i
pthread/*_safe.cil.c
pthread/*_safe.i
pthread-atomic/*_unsafe.i
pthread-atomic/*_safe.i

The benchmark set was provided by the ESBMC project.
Description: pthread, pthread-atomic

3. Control Flow and Integer Variables

The first category consists of two sub-categories, the verification tasks in the set ControlFlowInteger-MemSimple:

ntdrivers/*_unsafe.i.cil.c
ntdrivers/*_safe.i.cil.c
ssh/*_unsafe.i.cil.c
ssh/*_safe.i.cil.c

and the verification tasks in the set ControlFlowInteger-MemPrecise:

ntdrivers-simplified/*_unsafe.cil.c
ntdrivers-simplified/*_safe.cil.c
ssh-simplified/*_unsafe.cil.c
ssh-simplified/*_safe.cil.c
locks/*_unsafe.c
locks/*_safe.c

The former tasks are based on a simple memory model, in which variables can only be modified using direct assignments, or via pointer access if the address was obtained using the operator '&'. The latter tasks are based on a precise memory model, in which all memory cells can be written to, even dereferencing (uninitialized) pointers.

The problems in these two categories use programs and properties that depend mostly on control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency. The programs were taken from the source code repositories of the tools BLAST and CPAchecker.

4. Device Drivers Linux 64-bit

This category consists of problems that require the analysis of pointer aliases and function pointers (64-bit machine model):

ldv-drivers/*_unsafe*.cil.c
ldv-drivers/*_unsafe*.i
ldv-drivers/*_safe*.cil.c
ldv-drivers/*_safe*.i
ldv-linux-3.4/*_unsafe*.c
ldv-linux-3.4/*_safe*.c

The problems in this category were contributed by the Linux Driver Verification project.
Descriptions: ldv-drivers

5. Feature Checks

This category (previously called DeviceDrivers32) consists of problems that require the analysis of pointer aliases and function pointers (32-bit machine model):

ldv-regression/*_unsafe*.cil.c
ldv-regression/*_unsafe*.i
ldv-regression/*_safe*.cil.c
ldv-regression/*_safe*.i
ddv-machzwd/*_unsafe.cil.c
ddv-machzwd/*_unsafe.i
ddv-machzwd/*_safe.cil.c
ddv-machzwd/*_safe.i

The problems in this category were contributed by the Linux Driver Verification project and by the DDVerify project.
Descriptions: ldv-regression, ddv-machzwd

6. Heap Manipulation / Dynamic Data Structures

The problems in this category require the analysis of data structures on the heap and consist of the programs in the set HeapManipulation:

heap-manipulation/*_unsafe.cil.c
heap-manipulation/*_unsafe.i
heap-manipulation/*_safe.cil.c
heap-manipulation/*_safe.i
list-properties/*_safe.cil.c
list-properties/*_safe.i

The benchmarks in directory 'heap-manipulation' were provided by the Predator project and taken from a supplementary web page of the BLAST 3.0 project.
Description: heap-manipulation, list-properties

7. Loops

Some verification tasks for which loop analysis is necessary are contained in set Loops:

loops/*_unsafe.i
loops/*_safe.i

The benchmark set was provided by the ESBMC project.
Description: loops

8. Memory Safety

The category MemorySafety contains verification tasks for checking memory safety of programs:

memsafety/*_false-valid-deref.c
memsafety/*_false-valid-free.c
memsafety/*_false-valid-memtrack.c
memsafety/*_true.c

The benchmark set was provided by the Predator project.
Description: memsafety

9. Product Lines

The verification tasks in the set ProductLines are 'products' that are derived using different configurations of product lines:

product-lines/elevator*_unsafe.*.c
product-lines/elevator*_safe.*.c
product-lines/email*_unsafe.*.c
product-lines/email*_safe.*.c
product-lines/minepump*_unsafe.*.c
product-lines/minepump*_safe.*.c

The products were contributed by the SPLverifier project.
Description: product-lines

10. SystemC

This category contains problems that were derived from SystemC programs:

systemc/*_unsafe.cil.c
systemc/*_safe.cil.c

This set of benchmarks was provided by the SyCMC project. The programs were transformed to pure C programs by incorporating the scheduler into the C code.
Description: systemc

11. Overall

The category Overall contains all verification tasks of all above categories. (The weighting schema is explained on the rules page.)