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

The 2015 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.

1. Arrays

The set Arrays contains verification tasks for which treatment of arrays is necessary:

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

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

Memory Model: Precise
Architecture: 32 bit

2. Bit Vectors

The set BitVectors 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

3. 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

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

Memory Model: Precise
Architecture: 32 bit

4. Control Flow and Integer Variables

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

The first set, ControlFlowInteger, 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 second set, ECA, contains programs that represent event-condition-action systems.

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

The third set, Loops, 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

The fourth set of verification tasks, Product Lines, represent '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

5. 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-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

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

Memory Model: Simple
Architecture: 64 bit

6. Heap Manipulation / Dynamic Data Structures

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

7. Memory Safety

The category MemorySafety 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
memory-unsafe/*_false-valid-deref*.i
memory-unsafe/*_false-valid-free*.i
memory-unsafe/*_false-valid-memtrack*.i
memory-unsafe/*_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

8. Recursive

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

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

# For SV-COMP 2016:
# 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

9. Sequentialized Concurrent Programs

This category contains problems that were derived from SystemC programs:

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 programs were transformed to pure C programs by incorporating the scheduler into the C code. The other sequentialized programs are from the projects CSeq and HCCPS.
Descriptions: systemc, seq-mthreaded, seq-pthread

Memory Model: Precise
Architecture: 32 bit

10. Simple

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

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

The problems 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.

Memory Model: Simple
Architecture: 32 bit

11. 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

Description to be added.

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

Memory Model: Simple
Architecture: 32 bit

12. 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-memory-alloca/*_false-termination*.c.i
termination-memory-alloca/*_true-termination*.c.i
termination-numeric/*_false-termination*.c
termination-numeric/*_true-termination*.c

The verification tasks in this category were contributed by the Ultimate team and the AProVE team.
Descriptions: termination-crafted, termination-crafted-lit, termination-memory-alloca, termination-numeric

Memory Model: Simple
Architecture: 64 bit

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

Demonstration Categories (without Rankings)

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