Benchmark Verification Tasks

All verification tasks are available for web browsing and for download via the following GIT repository (for SV-COMP 2016 visit the tag 'svcomp16'): https://github.com/dbeyer/sv-benchmarks

The 2016 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 which memory model is used, and if the verification tasks assumes 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. Arrays

Category Arrays consists of two sub-categories.

ArraysReach

The set ArrayReach contains verification tasks for which treatment of arrays is necessary in order to determin reachability:

array-examples/*_false-unreach-call*.i
array-examples/*_true-unreach-call*.i

reducercommutativity/*_false-unreach-call*.i
reducercommutativity/*_true-unreach-call*.i

The benchmark set was provided by the projects BOOSTER and SAFARI.
Descriptions: array-examples.

Memory Model: Precise
Architecture: 32 bit

ArraysMemSafety

The set ArraysMemSafety contains verification tasks for checking memory safety of array-based programs:

array-memsafety/*_false-valid-deref*.i
# array-memsafety/*_false-valid-free*.i
# array-memsafety/*_false-valid-memtrack*.i
array-memsafety/*_true-valid-memsafety*.i

The benchmark set was provided by the project AProVE.
Description: arrays-memsafety

Memory Model: Precise
Architecture: 32 bit

2. Bit Vectors

This category consists of two sub-categories.

BitVectorsReach

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

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*.i
bitvector-regression/*_true-unreach-call*.i
bitvector-loops/*_false-unreach-call*.i
# bitvector-loops/*_true-unreach-call*.i

The benchmark set was provided by the projects Kratos and CPAchecker.
Descriptions: bitvector, bitvector-regression

Memory Model: Precise
Architecture: 32 bit

Overflows

The set Overflows contains verification tasks for checking if variables of type signed integers overflow (undefined behavior):

signedintegeroverflow-regression/*_false-no-overflow.c.i
signedintegeroverflow-regression/*_true-no-overflow.c.i

The benchmark set was contributed by the Ultimate team.
Description: overflows

Memory Model: Precise
Architecture: 64 bit

3. Heap Data Structures

This category consists of two sub-categories.

HeapReach

The problems in this set require the analysis of data structures on the heap, pointer aliases, and function pointers, and consist of the verification tasks in the set HeapManipulation:

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
ddv-machzwd/*_false-unreach-call*.i
ddv-machzwd/*_true-unreach-call*.i

The verification tasks in directory 'heap-manipulation' were provided by the Predator project and the verification tasks in directory 'list-properties' were taken from a supplementary web page of the BLAST 3.0 project. The problems in the directories 'ldv-regression' and 'ddv-machzwd' were contributed by the Linux Driver Verification project and by the DDVerify project, respectively.
Descriptions: heap-manipulation, list-properties, ldv-regression, ddv-machzwd

Memory Model: Precise
Architecture: 32 bit

HeapMemSafety

The set HeapMemSafety contains verification tasks for checking memory safety of programs:

memsafety/*_false-valid-deref*.i
memsafety/*_false-valid-free*.i
memsafety/*_false-valid-memtrack*.i
memsafety/*_true-valid-memsafety*.i
memsafety-ext/*_true-valid-memsafety*.i
list-ext-properties/*_false-valid-deref*.i
list-ext-properties/*_false-valid-free*.i
list-ext-properties/*_false-valid-memtrack*.i
list-ext-properties/*_true-valid-memsafety*.i
# memory-alloca/*_false-valid-deref*.i
# memory-alloca/*_false-valid-free*.i
# memory-alloca/*_false-valid-memtrack*.i
memory-alloca/*_true-valid-memsafety*.i
ldv-memsafety/*_false-valid-deref*.c
ldv-memsafety/*_true-valid-memsafety*.c
ldv-memsafety/*_false-valid-deref*.i
ldv-memsafety/*_false-valid-free*.i
ldv-memsafety/*_false-valid-memtrack*.i
ldv-memsafety/*_true-valid-memsafety*.i

The benchmark set was provided by the projects Predator and Forester.
Description: memsafety, memsafety-ext

Memory Model: Precise
Architecture: 32 bit

4. Floats

This category consists of the verification tasks in the set Floats:

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

The programs were contributed from the CBMC repository and by ASTREE developers.

Memory Model: Simple
Architecture: 32 bit

5. Integers and Control Flow

This category consists of the following sets of verification tasks. Each of these sets is an own subcategory.

ControlFlow

This set contains programs depend mostly on the control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency.

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

The programs were taken from the source code repositories of the tools BLAST and CPAchecker.

Memory Model: Precise
Architecture: 32 bit

Simple

The problems in this set 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.

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

Memory Model: Simple
Architecture: 32 bit

ECA (Event-Condition-Action Systems)

This set contains programs that represent event-condition-action systems.

eca-rers2012/*_false-unreach-call*.c
eca-rers2012/*_true-unreach-call*.c

Memory Model: Precise
Architecture: 32 bit

Loops

This set contains verification tasks for which loop analysis is necessary are contained:

loops/*_false-unreach-call*.i
loops/*_true-unreach-call*.i
loop-acceleration/*_false-unreach-call*.i
loop-acceleration/*_true-unreach-call*.i
loop-invgen/*_false-unreach-call*.i
loop-invgen/*_true-unreach-call*.i
loop-lit/*_true-unreach-call*.c.i
loop-new/*_true-unreach-call*.i

Memory Model: Precise
Architecture: 32 bit

Recursive

This set contains several verification tasks for which recursive analysis is necessary:

recursive/*_false-unreach-call*.c
recursive/*_true-unreach-call*.c
recursive-simple/*_false-unreach-call*.c
recursive-simple/*_true-unreach-call*.c

The benchmark set was provided by the Ultimate project.
Description: recursive

Memory Model: Precise
Architecture: 32 bit

ProductLines

This set of verification tasks represents 'products' and 'product simulators' that are derived using different configurations of product lines:

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

The directories 'ntdriver', 'ssh', and 'locks' were taken from the source code repositories of the tools BLAST and CPAchecker. The ECA programs were taken from the RERS Challenge 2012. The directory 'loops' was provided by the ESBMC project. The products were contributed by the SPLverifier project.
Descriptions: eca, loops, product-lines

Memory Model: Precise
Architecture: 32 bit

Sequentialized

This set contains sequentialized concurrent problems that were derived from SystemC programs. The programs were transformed to pure C programs by incorporating the scheduler into the C code.

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-pthread/*_false-unreach-call*.i
seq-pthread/*_true-unreach-call*.i

The SystemC benchmarks were provided by the SyCMC project. The other sequentialized programs are from the projects CSeq and HCCPS.
Descriptions: systemc, seq-mthreaded, seq-pthread

Memory Model: Precise
Architecture: 32 bit

6. Termination

This category contains the following verification tasks, for which the result is already known:

termination-crafted/*_false-termination*.c
termination-crafted/*_true-termination*.c
termination-crafted-lit/*_false-termination*.c
termination-crafted-lit/*_true-termination*.c
termination-libowfat/*_true-termination*.c.i
termination-memory-alloca/*_false-termination*.c.i
termination-memory-alloca/*_true-termination*.c.i
termination-numeric/*_true-termination*.c
termination-restricted-15/*_true-termination*.c
termination-restricted-15/*_false-termination*.c
termination-15/*_true-termination*.c.i
termination-15/*_false-termination*.c.i

The verification tasks in this category were contributed by the Ultimate team and the AProVE team.
Descriptions: to be added here termination

Memory Model: Simple
Architecture: 64 bit

7. Concurrency

Some concurrency problems are contained in the set Concurrency:

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

The benchmark set was provided by the projects ESBMC, Threader, and CProver.
Descriptions: pthread, pthread-atomic, pthread-ext

Memory Model: Precise
Architecture: 32 bit

8. DeviceDriversLinux64

This set consists of problems that require the analysis of pointer aliases and function pointers:

ldv-linux-3.0/*_false-unreach-call*.i
ldv-linux-3.0/*_true-unreach-call*.i
ldv-linux-3.4-simple/*_false-unreach-call*.c
ldv-linux-3.4-simple/*_true-unreach-call*.c
ldv-linux-3.7.3/*_false-unreach-call*.c
ldv-linux-3.7.3/*_true-unreach-call*.c
ldv-commit-tester/*_false-unreach-call*.c
ldv-commit-tester/*_true-unreach-call*.c
ldv-consumption/*_false-unreach-call*.c
ldv-consumption/*_true-unreach-call*.c
ldv-linux-3.12-rc1/*_false-unreach-call*.c
ldv-linux-3.12-rc1/*_true-unreach-call*.c
ldv-linux-3.16-rc1/*_false-unreach-call*.c
ldv-linux-3.16-rc1/*_true-unreach-call*.c
ldv-validator-v0.6/*_false-unreach-call*.c
ldv-validator-v0.8/*_false-unreach-call*.c
ldv-linux-4.2-rc1/*_false-unreach-call*.c
ldv-linux-4.2-rc1/*_true-unreach-call*.c
ldv-challenges/*_false-unreach-call*.c
ldv-challenges/*_true-unreach-call*.c

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

Memory Model: Simple
Architecture: 64 bit

9. Overall

The category Overall contains all verification tasks of all above categories. Each above-mentioned main category is an own subcategory in category Overall. (The weighting schema is explained on the rules page.)

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

Demonstration Categories (without Rankings)

... will be considered after the deadline for systems in the main categories.

BusyBox

The second set consists of problems from the software system BusyBox:

busybox-1.22.0/*_false-unreach-call.i
busybox-1.22.0/*_true-unreach-call.i

The problems in this category were contributed by Michael Tautschnig.
Descriptions: busybox-1.22.0

Memory Model: Precise
Architecture: 64 bit