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.