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
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
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
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
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
Some verification tasks for which loop analysis is necessary are contained in set 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
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
This category contains problems that were derived from SystemC programs:
The category Overall contains all verification tasks of all above categories. (The weighting schema is explained on the rules page.)