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:
termination-crafted,
termination-crafted-lit,
termination-libowfat,
termination-memory-alloca,
termination-numeric,
termination-restricted-15,
termination-15
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.
- Witness Validation for TRUE results
- Overflow Checking for all verification tasks
- Java programs (format: source code, if you need byte-code level, compile on the fly)
- Binaries (format: x86 32bit elf)
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