Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following SVN repository: https://svn.sosy-lab.org/software/sv-benchmarks/tags/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
Linux Device Drivers 64-bit
This category consists of problems that require the analysis of pointer aliases and function pointers (64-bit machine model):
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
Some concurrency problems are contained in the set Concurrency:
This category contains concurrency-related problems in the context of SystemC:
The category Overall contains all verification tasks of all above categories. (The jury has not yet determined a weighting schema.)