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

The 2012 edition of the competition on software verification is based on several categories of benchmark programs, which are explained in the following.

The benchmarks for this competition were contributed by several research and development groups. After the submission deadline for benchmarks, a group of people (organizer and participants) were working on improving the quality of the benchmark programs. That means that after the benchmark 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.

Control Flow and Integer Variables

The first set of verification tasks consists of the programs in the set ControlFlowInteger: 

ntdrivers-simplified/*_BUG.cil.c
ntdrivers-simplified/*[!G].cil.c
ntdrivers/*.BUG.i.cil.c
ntdrivers/*[!G].i.cil.c
ssh-simplified/*_BUG.cil.c
ssh-simplified/*[!G].cil.c
ssh/*.BUG.i.cil.c
ssh/*[!G].i.cil.c
locks/*.BUG.c
locks/*[!G].c

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

Linux Device Drivers 32-bit

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

ldv-regression/*-unsafe*.cil.c
ldv-regression/*-safe*.cil.c
ddv-machzwd/*_BUG.cil.c
ddv-machzwd/*[!G].cil.c

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

Linux Device Drivers 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/*-safe*.cil.c

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

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/*BUG.cil.c
heap-manipulation/*[!G].cil.c
list-properties/*.cil.c

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

Concurrency

Some concurrency problems are contained in the set Concurrency: 

pthread/*BUG.cil.c
pthread/*[!G].cil.c

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

SystemC

This category contains concurrency-related problems in the context of SystemC: 

systemc/*BUG.cil.c
systemc/*[!G].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

Overall

The category Overall contains all verification tasks of all above categories. (The jury has not yet determined a weighting schema.)