SV-COMP 2018 - 7th International Competition on Software Verification

Benchmark Verification Tasks

All verification tasks are available for web browsing and for download via the following GIT repository: (for SV-COMP 2018 visit the tag 'svcomp18'): https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks

This 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 whether its verification tasks assume 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. ReachSafety

This category consists of the following sub-categories.

ReachSafety-Arrays

Contains verification tasks for which treatment of arrays is necessary in order to determine reachability.

Verification tasks consist of the programs that match

array-examples/*_false-unreach-call*.i
array-examples/*_true-unreach-call*.i

array-industry-pattern/*_false-unreach-call*.i
array-industry-pattern/*_true-unreach-call*.i

reducercommutativity/*_false-unreach-call*.i
reducercommutativity/*_true-unreach-call*.i

array-tiling/*_false-unreach-call*.i
array-tiling/*_true-unreach-call*.i

array-programs/*_false-unreach-call*.i
array-programs/*_true-unreach-call*.i

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-BitVectors

Contains verification tasks for which treatment of bit-operations is necessary.

Verification tasks consist of the programs that match

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*.c
bitvector-regression/*_true-unreach-call*.c
bitvector-loops/*_false-unreach-call*.i
# bitvector-loops/*_true-unreach-call*.i

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-ControlFlow

Contains programs for which the correctness depends mostly on the control-flow structure and integer variables. There is no particular focus on pointers, data structures, and concurrency.

Verification tasks consist of the programs that match

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

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

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-ECA

Contains programs that represent event-condition-action systems.

Verification tasks consist of the programs that match

eca-rers2012/*_false-unreach-call*.c
eca-rers2012/*_true-unreach-call*.c
psyco/*_false-unreach-call*.c
psyco/*_true-unreach-call*.c

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-Floats

Contains verification tasks for checking programs with floating-point arithmetics.

Verification tasks consist of the programs that match

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
floats-esbmc-regression/*_true-unreach-call*.i
floats-esbmc-regression/*_false-unreach-call*.i

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-Heap

Contains verification tasks that require the analysis of data structures on the heap, pointer aliases, and function pointers.

Verification tasks consist of the programs that match

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
ldv-regression/test[0-9][0-9]_false-unreach-call*.c
ldv-regression/test[0-9][0-9]_true-unreach-call*.c
ddv-machzwd/*_false-unreach-call*.i
ddv-machzwd/*_true-unreach-call*.i

forester-heap/*_false-unreach-call*.i
forester-heap/*_true-unreach-call*.i

list-ext-properties/*_false-unreach-call*.i
list-ext2-properties/*-unreach-call*.i

ldv-sets/*_false-unreach-call*.i
ldv-sets/*_true-unreach-call*.i

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-Loops

Contains verification tasks for which loop analysis is necessary.

Verification tasks consist of the programs that match

loops/*_false-unreach-call*.i
loops/*_true-unreach-call*.i
loop-acceleration/*_false-unreach-call*.i
loop-acceleration/*_true-unreach-call*.i
loop-crafted/*_false-unreach-call*.i
loop-crafted/*_true-unreach-call*.i

loop-invgen/*_false-unreach-call*.i
loop-invgen/*_true-unreach-call*.i
loop-lit/*_true-unreach-call*.i
loop-lit/*_false-unreach-call*.i
loop-new/*_true-unreach-call*.i
loop-industry-pattern/*_true-unreach-call*.c

loops/heavy_true-unreach-call.c
loops/compact_false-unreach-call.c
loops/heavy_false-unreach-call.c

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-ProductLines

Contains programs that represents 'products' and 'product simulators' that are derived using different configurations of product lines.

Verification tasks consist of the programs that match

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

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-Recursive

Contains verification tasks for which recursive analysis is necessary.

Verification tasks consist of the programs that match

recursive/*_false-unreach-call*.c
recursive/*_true-unreach-call*.c
recursive-simple/*_false-unreach-call*.c
recursive-simple/*_true-unreach-call*.c

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

ReachSafety-Sequentialized

Contains sequentialized concurrent programs that were derived from SystemC programs. The programs were transformed to pure C programs by incorporating the scheduler into the C code.

Verification tasks consist of the programs that match

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

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

2. MemSafety

This category consists of the following sub-categories.

MemSafety-Arrays

Contains verification tasks for checking memory safety of array-based programs.

Verification tasks consist of the programs that match

array-memsafety/*_false-valid-deref*.i
# array-memsafety/*_false-valid-free*.i
# array-memsafety/*_false-valid-memtrack*.i
array-memsafety/*_true-valid-memsafety*.i

array-examples/*_false-valid-deref*.i
#array-examples/*_true-valid-memsafety*.i

with the specification

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )

and the following parameter:

Architecture: 32 bit

MemSafety-Heap

Contains verification tasks for checking memory safety of programs.

Verification tasks consist of the programs that match

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
memsafety-ext2/*_false-valid-deref*.i
memsafety-ext2/*_false-valid-memtrack*.i
memsafety-ext2/*_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
ldv-memsafety-bitfields/*_true-valid-memsafety*.i
ldv-memsafety-bitfields/*_false-valid-deref*.i
ldv-memsafety-bitfields/*_false-valid-free*.i

with the specification

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )

and the following parameter:

Architecture: 32 bit

MemSafety-LinkedLists

Contains verification tasks for checking memory safety of programs.

Verification tasks consist of the programs that match

heap-manipulation/*_true-valid-memsafety*.i
heap-manipulation/*_false-valid-deref*.i
heap-manipulation/*_false-valid-memtrack*.i
forester-heap/*_false-valid-memtrack*.i
list-properties/*_true-valid-memsafety*.i
list-properties/*_false-valid-memtrack*.i
ddv-machzwd/*_true-valid-memsafety*.i
ddv-machzwd/*_false-valid-memtrack*.i
forester-heap/*_true-valid-memsafety*.i
forester-heap/*_false-valid-deref*.i

with the specification

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )

and the following parameter:

Architecture: 32 bit

MemSafety-Other

Contains verification tasks for checking memory safety of programs.

Verification tasks consist of the programs that match

loop-acceleration/*_false-valid-deref*.i
ntdrivers/*_false-valid-deref*.i.cil.c
ntdrivers-simplified/*_true-valid-memsafety*.cil.c
locks/*_true-valid-memsafety*.c

with the specification

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )

and the following parameter:

Architecture: 32 bit

3. ConcurrencySafety

This category consists of the following sub-categories.

ConcurrencySafety-Main

Contains concurrency problems.

Verification tasks consist of the programs that match

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
pthread-complex/*_false-unreach-call*.i
pthread-complex/*_true-unreach-call*.i
pthread-driver-races/*_true-unreach-call*.i
pthread-driver-races/*_false-unreach-call*.i
pthread-C-DAC/*_true-unreach-call*.i
pthread-C-DAC/*_false-unreach-call*.i

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 32 bit

4. NoOverflows

This category consists of the following sub-categories.

NoOverflows-BitVectors

Contains verification tasks for checking if variables of type signed integers overflow.

Verification tasks consist of the programs that match

signedintegeroverflow-regression/*_false-no-overflow*.c.i
signedintegeroverflow-regression/*_true-no-overflow*.c.i

termination-crafted/*_false-no-overflow*.c
termination-crafted/*_true-no-overflow*.c

termination-crafted-lit/*_false-no-overflow*.c
termination-crafted-lit/*_true-no-overflow*.c

termination-numeric/*_false-no-overflow*.c
termination-numeric/*_true-no-overflow*.c

with the specification

CHECK( init(main()), LTL(G ! overflow) )

and the following parameter:

Architecture: 64 bit

NoOverflows-Other

Contains verification tasks for checking if variables of type signed integers overflow.

Verification tasks consist of the programs that match

recursive/*_false-no-overflow*.c
recursive/*_true-no-overflow*.c
recursive-simple/*_false-no-overflow*.c
recursive-simple/*_true-no-overflow*.c
bitvector/*_false-no-overflow*.i
bitvector/*_true-no-overflow*.i

with the specification

CHECK( init(main()), LTL(G ! overflow) )

and the following parameter:

Architecture: 32 bit

5. Termination

This category consists of the following sub-categories.

Termination-MainControlFlow

Contains programs for which termination should be decided.

Verification tasks consist of the programs that match

termination-crafted/*_false-termination*.c
termination-crafted/*_true-termination*.c
termination-crafted-lit/*_false-termination*.c
termination-crafted-lit/*_true-termination*.c
termination-numeric/*_true-termination*.c
termination-restricted-15/*_true-termination*.c
termination-restricted-15/*_false-termination*.c

with the specification

CHECK( init(main()), LTL(F end) )

and the following parameter:

Architecture: 64 bit

Termination-MainHeap

Contains programs for which termination should be decided.

Verification tasks consist of the programs that match

termination-libowfat/*_true-termination*.c.i
termination-memory-alloca/*_false-termination*.c.i
termination-memory-alloca/*_true-termination*.c.i
termination-memory-linkedlists/*_false-termination*.c.i
termination-memory-linkedlists/*_true-termination*.c.i
termination-15/*_true-termination*.c.i
termination-15/*_false-termination*.c.i
termination-recursive-malloc/*_true-termination*.c.i

with the specification

CHECK( init(main()), LTL(F end) )

and the following parameter:

Architecture: 64 bit

Termination-Other

Contains programs for which termination should be decided.

Verification tasks consist of the programs that match

# from ReachSafety-Arrays
array-examples/*_true-termination*.i
array-industry-pattern/*_true-termination*.i

# from ReachSafety-BitVectors
bitvector/*_false-termination*.i
bitvector/*_true-termination*.i
bitvector/*_false-termination*.BV.c.cil.c
bitvector/*_true-termination*.c.cil.c
bitvector-regression/*_true-termination*.c
bitvector-loops/*_true-termination*.i

# from ReachSafety-ControlFlow
ntdrivers-simplified/*_true-termination*.cil.c
ssh-simplified/*_false-termination*.cil.c
ssh-simplified/*_true-termination*.cil.c
locks/*_false-termination*.c
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c
ntdrivers/*_true-termination*.i.cil.c

# from ReachSafety-ECA
eca-rers2012/*_false-termination*.c
psyco/*_false-termination.c

# from ReachSafety-Floats
floats-cdfpl/*_true-termination*.i
floats-cbmc-regression/*_true-termination*.i

# from ReachSafety-Heap
ldv-regression/*_true-termination*.i
ldv-regression/*_false-termination*.i
ldv-regression/test[0-9][0-9]*_true-termination*.c
list-ext-properties/*_true-termination*.i
list-ext2-properties/*_false-termination*.i
ldv-sets/*_true-termination*.i

# from ReachSafety-Loops
loops/*_false-termination*.i
loops/*_true-termination*.i
loop-acceleration/*_true-termination*.i
loop-acceleration/*_false-termination*.i
loop-invgen/*_false-termination*.i
loop-invgen/*_true-termination*.i
loop-lit/*_true-termination*.i
loop-lit/*_false-termination*.i
loop-new/*_true-termination*.i

# from ReachSafety-ProductLines
product-lines/*_true-termination*.c
product-lines/*_false-termination*.c

# from ReachSafety-Recursive
recursive/*_false-termination*.c
recursive/*_true-termination*.c
recursive-simple/*_true-termination*.c

# from ReachSafety-Sequentialized
systemc/*_false-termination*.cil.c
seq-mthreaded/*_true-termination*.c
seq-pthread/*_true-termination*.i

# from ReachSafety-Arrays
reducercommutativity/*_true-termination*.i

# from MemSafety-Arrays
array-memsafety/*_true-termination*.i

# from MemSafety-Heap
memsafety/*_true-termination*.i
memsafety/*_false-termination*.i
memsafety-ext/*_false-termination*.i
ldv-memsafety/*_true-termination*.c
ldv-memsafety/*_true-termination*.i
ldv-memsafety-bitfields/*_true-termination*.i


# from Concurrency
pthread-atomic/*_true-termination*.i


# from NoOverflows-BitVectors
# is 64bit and needs own category 
# signedintegeroverflow-regression/*true-termination*.c.i

with the specification

CHECK( init(main()), LTL(F end) )

and the following parameter:

Architecture: 32 bit

6. SoftwareSystems

This category consists of several sets of verification tasks. Each of these sets is an own subcategory. While the categories above are collections of rather `academic', or synthetisized, example verification tasks, this category aims to represent verification tasks from real software systems.

Systems_BusyBox_MemSafety

Contains problems from the software system BusyBox.

Verification tasks consist of the programs that match

busybox-1.22.0/*_false-valid-deref*.i
#busybox-1.22.0/*_false-valid-free*.i
busybox-1.22.0/*_false-valid-memtrack*.i
busybox-1.22.0/*_true-valid-memsafety*.i

with the specification

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )

and the following parameter:

Architecture: 64 bit

Systems_BusyBox_Overflows

Verification tasks consist of the programs that match

with the specification

and the following parameter:

Architecture:

Systems_DeviceDriversLinux64_ReachSafety

Contains problems that require the analysis of pointer aliases and function pointers.

Verification tasks consist of the programs that match

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
ldv-linux-3.14/*_false-unreach-call*.c
ldv-linux-3.14/*_true-unreach-call*.c
ldv-linux-4.0-rc1-mav/*_false-unreach-call*.c
ldv-linux-4.0-rc1-mav/*_true-unreach-call*.c

with the specification

CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )

and the following parameter:

Architecture: 64 bit

7. 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.)

8. 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.)

	TACAS 2018
Competition on Software Verification (SV-COMP)