Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following Git repository: (for SV-COMP 2025 visit the tag 'svcomp25'): 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 who 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 verification task, we specify whether it assume a 32-bit or a 64-bit architecture.
For illustration, a structured overview (2025) shows the categories below.
Rankings will be provided for the first- and second-level categories,
and FalsificationOverall, which is not shown in the figure.
The authorative definition of the category structure (from which this web page is generated) is maintained in the repository for the benchmark definitions (https://gitlab.com/sosy-lab/sv-comp/bench-defs).
1. ReachSafety
ReachSafety-Arrays
The verification tasks consist of the programs that match
# sv-benchmarks/c/Arrays.set # array-examples/*.yml array-industry-pattern/*.yml reducercommutativity/*.yml array-tiling/*.yml array-programs/*.yml array-crafted/*.yml array-multidimensional/*.yml array-patterns/*.yml array-cav19/*.yml array-lopstr16/*.yml array-fpi/*.yml array-memsafety/*.yml array-memsafety-realloc/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-BitVectors
The verification tasks consist of the programs that match
# sv-benchmarks/c/BitVectors.set # bitvector/*.yml bitvector-regression/*.yml bitvector-loops/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-ControlFlow
The verification tasks consist of the programs that match
# sv-benchmarks/c/ControlFlow.set # ntdrivers-simplified/*.yml openssl-simplified/*.yml locks/*.yml ntdrivers/*.yml openssl/*.yml memory-model/*.yml unsignedintegeroverflow-sas23/*.yml longjmp/*.yml signedintegeroverflow-regression/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-ECA
The verification tasks consist of the programs that match
# sv-benchmarks/c/ECA.set # eca-rers2012/*.yml eca-rers2018/*.yml psyco/*.yml eca-programs/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Floats
The verification tasks consist of the programs that match
# sv-benchmarks/c/Floats.set # floats-cdfpl/*.yml floats-cbmc-regression/*.yml float-benchs/*.yml floats-esbmc-regression/*.yml float-newlib/*.yml loop-floats-scientific-comp/*.yml neural-networks/*.yml floats-nonlinear/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Heap
The verification tasks consist of the programs that match
# sv-benchmarks/c/Heap.set # ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml heap-data/*.yml memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml memsafety-ext3/*.yml memsafety-bftpd/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
# sv-benchmarks/c/LinkedLists.set # memsafety-broom/*.yml heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml ddv-machzwd/*.yml list-simple/*.yml list-ext3-properties/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Loops
The verification tasks consist of the programs that match
# sv-benchmarks/c/Loops.set # loops/*.yml loop-acceleration/*.yml loop-crafted/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml loop-industry-pattern/*.yml loops-crafted-1/*.yml loop-invariants/*.yml loop-invariants64/*.yml loop-simple/*.yml loop-zilu/*.yml nla-digbench/*.yml nla-digbench-scaling/*.yml
# sv-benchmarks/c/VerifyThis-Loops.set # verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/tree_del_iter.yml verifythis/tree_del_iter_incorrect.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-ProductLines
The verification tasks consist of the programs that match
# sv-benchmarks/c/ProductLines.set # product-lines/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Recursive
The verification tasks consist of the programs that match
# sv-benchmarks/c/Recursive.set # recursive/*.yml recursive-simple/*.yml recursive-with-pointer/*.yml recursified_loop-crafted/*.yml recursified_loop-invariants/*.yml recursified_loop-simple/*.yml recursified_nla-digbench/*.yml
# sv-benchmarks/c/VerifyThis-Recursive.set # verifythis/prefixsum_rec.yml verifythis/tree_del_rec.yml verifythis/tree_del_rec_incorrect.yml verifythis/tree_max.yml verifythis/tree_max_incorrect.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Sequentialized
The verification tasks consist of the programs that match
# sv-benchmarks/c/Sequentialized.set # systemc/*.yml seq-mthreaded/*.yml seq-mthreaded-reduced/*.yml seq-pthread/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-XCSP
The verification tasks consist of the programs that match
# sv-benchmarks/c/XCSP.set # xcsp/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Combinations
The verification tasks consist of the programs that match
# sv-benchmarks/c/Combinations.set # combinations/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Hardware
The verification tasks consist of the programs that match
# sv-benchmarks/c/Hardware.set # hardware-verification-array/btor2c-lazyMod.*.yml hardware-verification-bv/btor2c-lazyMod.*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Hardness
The verification tasks consist of the programs that match
# sv-benchmarks/c/Hardness.set # hardness-nfm22/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ReachSafety-Fuzzle
The verification tasks consist of the programs that match
# sv-benchmarks/c/Fuzzle.set # fuzzle-programs/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
2. MemSafety
MemSafety-Arrays
The verification tasks consist of the programs that match
# sv-benchmarks/c/Arrays.set # array-examples/*.yml array-industry-pattern/*.yml reducercommutativity/*.yml array-tiling/*.yml array-programs/*.yml array-crafted/*.yml array-multidimensional/*.yml array-patterns/*.yml array-cav19/*.yml array-lopstr16/*.yml array-fpi/*.yml array-memsafety/*.yml array-memsafety-realloc/*.yml
# sv-benchmarks/c/Heap-Termination.set # termination-dietlibc/*.yml termination-memory-alloca/*.yml termination-memory-linkedlists/*.yml termination-15/*.yml termination-recursive-malloc/*.yml
# sv-benchmarks/c/VerifyThis-Loops.set # verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/tree_del_iter.yml verifythis/tree_del_iter_incorrect.yml
# sv-benchmarks/c/VerifyThis-Recursive.set # verifythis/prefixsum_rec.yml verifythis/tree_del_rec.yml verifythis/tree_del_rec_incorrect.yml verifythis/tree_max.yml verifythis/tree_max_incorrect.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
MemSafety-Heap
The verification tasks consist of the programs that match
# sv-benchmarks/c/Heap.set # ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml heap-data/*.yml memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml memsafety-ext3/*.yml memsafety-bftpd/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
MemSafety-LinkedLists
The verification tasks consist of the programs that match
# sv-benchmarks/c/LinkedLists.set # memsafety-broom/*.yml heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml ddv-machzwd/*.yml list-simple/*.yml list-ext3-properties/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
MemSafety-Other
The verification tasks consist of the programs that match
# sv-benchmarks/c/Loops.set # loops/*.yml loop-acceleration/*.yml loop-crafted/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml loop-industry-pattern/*.yml loops-crafted-1/*.yml loop-invariants/*.yml loop-invariants64/*.yml loop-simple/*.yml loop-zilu/*.yml nla-digbench/*.yml nla-digbench-scaling/*.yml
# sv-benchmarks/c/ControlFlow.set # ntdrivers-simplified/*.yml openssl-simplified/*.yml locks/*.yml ntdrivers/*.yml openssl/*.yml memory-model/*.yml unsignedintegeroverflow-sas23/*.yml longjmp/*.yml signedintegeroverflow-regression/*.yml
# sv-benchmarks/c/ControlFlow-Termination.set # termination-crafted/*.yml termination-crafted-lit/*.yml termination-numeric/*.yml termination-restricted-15/*.yml termination-nla/*.yml
# sv-benchmarks/c/Recursive.set # recursive/*.yml recursive-simple/*.yml recursive-with-pointer/*.yml recursified_loop-crafted/*.yml recursified_loop-invariants/*.yml recursified_loop-simple/*.yml recursified_nla-digbench/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
MemSafety-Juliet
The verification tasks consist of the programs that match
# sv-benchmarks/c/Juliet.set # Juliet_Test/CWE415*.yml Juliet_Test/CWE476*_int*.yml Juliet_Test/CWE476*_long*.yml Juliet_Test/CWE476*_struct*.yml Juliet_Test/CWE121*rand*.yml Juliet_Test/CWE121*fgets*.yml Juliet_Test/CWE121*large*.yml Juliet_Test/CWE401*__int*.yml Juliet_Test/CWE401*__struct*.yml Juliet_Test/CWE401*__twoIntsStruct*.yml Juliet_Test/CWE590*.yml Juliet_Test/CWE190_Integer_Overflow__int*.yml Juliet_Test/CWE191_Integer_Underflow__int*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
MemSafety-MemCleanup
The verification tasks consist of the programs that match
# sv-benchmarks/c/Heap.set # ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml heap-data/*.yml memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml memsafety-ext3/*.yml memsafety-bftpd/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
# sv-benchmarks/c/Juliet.set # Juliet_Test/CWE415*.yml Juliet_Test/CWE476*_int*.yml Juliet_Test/CWE476*_long*.yml Juliet_Test/CWE476*_struct*.yml Juliet_Test/CWE121*rand*.yml Juliet_Test/CWE121*fgets*.yml Juliet_Test/CWE121*large*.yml Juliet_Test/CWE401*__int*.yml Juliet_Test/CWE401*__struct*.yml Juliet_Test/CWE401*__twoIntsStruct*.yml Juliet_Test/CWE590*.yml Juliet_Test/CWE190_Integer_Overflow__int*.yml Juliet_Test/CWE191_Integer_Underflow__int*.yml
# sv-benchmarks/c/LinkedLists.set # memsafety-broom/*.yml heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml ddv-machzwd/*.yml list-simple/*.yml list-ext3-properties/*.yml
# sv-benchmarks/c/VerifyThis-Loops.set # verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/tree_del_iter.yml verifythis/tree_del_iter_incorrect.yml
# sv-benchmarks/c/VerifyThis-Recursive.set # verifythis/prefixsum_rec.yml verifythis/tree_del_rec.yml verifythis/tree_del_rec_incorrect.yml verifythis/tree_max.yml verifythis/tree_max_incorrect.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
with the specification:
CHECK( init(main()), LTL(G valid-memcleanup) )
3. ConcurrencySafety
ConcurrencySafety-Main
The verification tasks consist of the programs that match
# sv-benchmarks/c/Concurrency.set # pthread/*.yml pthread-atomic/*.yml pthread-ext/*.yml pthread-wmm/*.yml pthread-lit/*.yml ldv-races/*.yml ldv-linux-3.14-races/*.yml pthread-complex/*.yml pthread-driver-races/*.yml pthread-C-DAC/*.yml pthread-divine/*.yml pthread-nondet/*.yml goblint-regression/*.yml weaver/*.yml pthread-deagle/*.yml pthread-race-challenges/*.yml pthread-memsafety/*.yml libvsync/*.yml pthread-theta/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
ConcurrencySafety-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/Concurrency.set # pthread/*.yml pthread-atomic/*.yml pthread-ext/*.yml pthread-wmm/*.yml pthread-lit/*.yml ldv-races/*.yml ldv-linux-3.14-races/*.yml pthread-complex/*.yml pthread-driver-races/*.yml pthread-C-DAC/*.yml pthread-divine/*.yml pthread-nondet/*.yml goblint-regression/*.yml weaver/*.yml pthread-deagle/*.yml pthread-race-challenges/*.yml pthread-memsafety/*.yml libvsync/*.yml pthread-theta/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
ConcurrencySafety-NoOverflows
The verification tasks consist of the programs that match
# sv-benchmarks/c/Concurrency.set # pthread/*.yml pthread-atomic/*.yml pthread-ext/*.yml pthread-wmm/*.yml pthread-lit/*.yml ldv-races/*.yml ldv-linux-3.14-races/*.yml pthread-complex/*.yml pthread-driver-races/*.yml pthread-C-DAC/*.yml pthread-divine/*.yml pthread-nondet/*.yml goblint-regression/*.yml weaver/*.yml pthread-deagle/*.yml pthread-race-challenges/*.yml pthread-memsafety/*.yml libvsync/*.yml pthread-theta/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
NoDataRace-Main
The verification tasks consist of the programs that match
# sv-benchmarks/c/Concurrency.set # pthread/*.yml pthread-atomic/*.yml pthread-ext/*.yml pthread-wmm/*.yml pthread-lit/*.yml ldv-races/*.yml ldv-linux-3.14-races/*.yml pthread-complex/*.yml pthread-driver-races/*.yml pthread-C-DAC/*.yml pthread-divine/*.yml pthread-nondet/*.yml goblint-regression/*.yml weaver/*.yml pthread-deagle/*.yml pthread-race-challenges/*.yml pthread-memsafety/*.yml libvsync/*.yml pthread-theta/*.yml
with the specification:
CHECK( init(main()), LTL(G ! data-race) )
4. NoOverflows
NoOverflows-Main
The verification tasks consist of the programs that match
# sv-benchmarks/c/Arrays.set # array-examples/*.yml array-industry-pattern/*.yml reducercommutativity/*.yml array-tiling/*.yml array-programs/*.yml array-crafted/*.yml array-multidimensional/*.yml array-patterns/*.yml array-cav19/*.yml array-lopstr16/*.yml array-fpi/*.yml array-memsafety/*.yml array-memsafety-realloc/*.yml
# sv-benchmarks/c/BitVectors.set # bitvector/*.yml bitvector-regression/*.yml bitvector-loops/*.yml
# sv-benchmarks/c/BitVectors-Termination.set # termination-bwb/*.yml
# sv-benchmarks/c/ControlFlow.set # ntdrivers-simplified/*.yml openssl-simplified/*.yml locks/*.yml ntdrivers/*.yml openssl/*.yml memory-model/*.yml unsignedintegeroverflow-sas23/*.yml longjmp/*.yml signedintegeroverflow-regression/*.yml
# sv-benchmarks/c/ControlFlow-Termination.set # termination-crafted/*.yml termination-crafted-lit/*.yml termination-numeric/*.yml termination-restricted-15/*.yml termination-nla/*.yml
# sv-benchmarks/c/ECA.set # eca-rers2012/*.yml eca-rers2018/*.yml psyco/*.yml eca-programs/*.yml
# sv-benchmarks/c/Floats.set # floats-cdfpl/*.yml floats-cbmc-regression/*.yml float-benchs/*.yml floats-esbmc-regression/*.yml float-newlib/*.yml loop-floats-scientific-comp/*.yml neural-networks/*.yml floats-nonlinear/*.yml
# sv-benchmarks/c/Heap.set # ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml heap-data/*.yml memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml memsafety-ext3/*.yml memsafety-bftpd/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
# sv-benchmarks/c/Heap-Termination.set # termination-dietlibc/*.yml termination-memory-alloca/*.yml termination-memory-linkedlists/*.yml termination-15/*.yml termination-recursive-malloc/*.yml
# sv-benchmarks/c/LinkedLists.set # memsafety-broom/*.yml heap-manipulation/*.yml forester-heap/*.yml list-properties/*.yml ddv-machzwd/*.yml list-simple/*.yml list-ext3-properties/*.yml
# sv-benchmarks/c/Loops.set # loops/*.yml loop-acceleration/*.yml loop-crafted/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml loop-industry-pattern/*.yml loops-crafted-1/*.yml loop-invariants/*.yml loop-invariants64/*.yml loop-simple/*.yml loop-zilu/*.yml nla-digbench/*.yml nla-digbench-scaling/*.yml
# sv-benchmarks/c/Recursive.set # recursive/*.yml recursive-simple/*.yml recursive-with-pointer/*.yml recursified_loop-crafted/*.yml recursified_loop-invariants/*.yml recursified_loop-simple/*.yml recursified_nla-digbench/*.yml
# sv-benchmarks/c/Sequentialized.set # systemc/*.yml seq-mthreaded/*.yml seq-mthreaded-reduced/*.yml seq-pthread/*.yml
# sv-benchmarks/c/VerifyThis-Loops.set # verifythis/duplets.yml verifythis/elimination_max.yml verifythis/lcp.yml verifythis/prefixsum_iter.yml verifythis/tree_del_iter.yml verifythis/tree_del_iter_incorrect.yml
# sv-benchmarks/c/VerifyThis-Recursive.set # verifythis/prefixsum_rec.yml verifythis/tree_del_rec.yml verifythis/tree_del_rec_incorrect.yml verifythis/tree_max.yml verifythis/tree_max_incorrect.yml verifythis/elimination_max_rec.yml verifythis/elimination_max_rec_onepoint.yml
# sv-benchmarks/c/XCSP.set # xcsp/*.yml
# sv-benchmarks/c/SoftwareSystems-AWS-C-Common.set # aws-c-common/*.yml
# sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set # ldv-linux-3.0/*.yml ldv-linux-3.4-simple/*.yml ldv-linux-3.7.3/*.yml ldv-commit-tester/*.yml ldv-consumption/*.yml ldv-linux-3.12-rc1/*.yml ldv-linux-3.16-rc1/*.yml ldv-validator-v0.6/*.yml ldv-validator-v0.8/*.yml ldv-linux-4.2-rc1/*.yml ldv-linux-3.14/*.yml ldv-challenges/*.yml ldv-linux-4.0-rc1-mav/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
NoOverflows-Juliet
The verification tasks consist of the programs that match
# sv-benchmarks/c/Juliet.set # Juliet_Test/CWE415*.yml Juliet_Test/CWE476*_int*.yml Juliet_Test/CWE476*_long*.yml Juliet_Test/CWE476*_struct*.yml Juliet_Test/CWE121*rand*.yml Juliet_Test/CWE121*fgets*.yml Juliet_Test/CWE121*large*.yml Juliet_Test/CWE401*__int*.yml Juliet_Test/CWE401*__struct*.yml Juliet_Test/CWE401*__twoIntsStruct*.yml Juliet_Test/CWE590*.yml Juliet_Test/CWE190_Integer_Overflow__int*.yml Juliet_Test/CWE191_Integer_Underflow__int*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
5. Termination
Termination-BitVectors
The verification tasks consist of the programs that match
# sv-benchmarks/c/BitVectors-Termination.set # termination-bwb/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
Termination-MainControlFlow
The verification tasks consist of the programs that match
# sv-benchmarks/c/ControlFlow-Termination.set # termination-crafted/*.yml termination-crafted-lit/*.yml termination-numeric/*.yml termination-restricted-15/*.yml termination-nla/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
Termination-MainHeap
The verification tasks consist of the programs that match
# sv-benchmarks/c/Heap-Termination.set # termination-dietlibc/*.yml termination-memory-alloca/*.yml termination-memory-linkedlists/*.yml termination-15/*.yml termination-recursive-malloc/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
Termination-Other
The verification tasks consist of the programs that match
# sv-benchmarks/c/Arrays.set # array-examples/*.yml array-industry-pattern/*.yml reducercommutativity/*.yml array-tiling/*.yml array-programs/*.yml array-crafted/*.yml array-multidimensional/*.yml array-patterns/*.yml array-cav19/*.yml array-lopstr16/*.yml array-fpi/*.yml array-memsafety/*.yml array-memsafety-realloc/*.yml
# sv-benchmarks/c/BitVectors.set # bitvector/*.yml bitvector-regression/*.yml bitvector-loops/*.yml
# sv-benchmarks/c/ControlFlow.set # ntdrivers-simplified/*.yml openssl-simplified/*.yml locks/*.yml ntdrivers/*.yml openssl/*.yml memory-model/*.yml unsignedintegeroverflow-sas23/*.yml longjmp/*.yml signedintegeroverflow-regression/*.yml
# sv-benchmarks/c/ECA.set # eca-rers2012/*.yml eca-rers2018/*.yml psyco/*.yml eca-programs/*.yml
# sv-benchmarks/c/Floats.set # floats-cdfpl/*.yml floats-cbmc-regression/*.yml float-benchs/*.yml floats-esbmc-regression/*.yml float-newlib/*.yml loop-floats-scientific-comp/*.yml neural-networks/*.yml floats-nonlinear/*.yml
# sv-benchmarks/c/Heap.set # ldv-regression/*.yml list-ext-properties/*.yml list-ext2-properties/*.yml ldv-sets/*.yml heap-data/*.yml memsafety/*.yml memsafety-ext/*.yml memsafety-ext2/*.yml memsafety-ext3/*.yml memsafety-bftpd/*.yml memory-alloca/*.yml ldv-memsafety/*.yml ldv-memsafety-bitfields/*.yml
# sv-benchmarks/c/Loops.set # loops/*.yml loop-acceleration/*.yml loop-crafted/*.yml loop-invgen/*.yml loop-lit/*.yml loop-new/*.yml loop-industry-pattern/*.yml loops-crafted-1/*.yml loop-invariants/*.yml loop-invariants64/*.yml loop-simple/*.yml loop-zilu/*.yml nla-digbench/*.yml nla-digbench-scaling/*.yml
# sv-benchmarks/c/ProductLines.set # product-lines/*.yml
# sv-benchmarks/c/Recursive.set # recursive/*.yml recursive-simple/*.yml recursive-with-pointer/*.yml recursified_loop-crafted/*.yml recursified_loop-invariants/*.yml recursified_loop-simple/*.yml recursified_nla-digbench/*.yml
# sv-benchmarks/c/Sequentialized.set # systemc/*.yml seq-mthreaded/*.yml seq-mthreaded-reduced/*.yml seq-pthread/*.yml
# sv-benchmarks/c/SoftwareSystems-uthash.set # uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
6. SoftwareSystems
This category consists of several sets of verification tasks. Each of these sets is an own sub-category. While the categories above are collections of rather `academic', or synthesized, example verification tasks, this category aims to represent verification tasks from real software systems.
SoftwareSystems-AWS-C-Common-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-AWS-C-Common.set # aws-c-common/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
SoftwareSystems-coreutils-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
SoftwareSystems-coreutils-NoOverflows
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
SoftwareSystems-BusyBox-NoOverflows
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-BusyBox.set # busybox-1.22.0/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
SoftwareSystems-DeviceDriversLinux64-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set # ldv-linux-3.0/*.yml ldv-linux-3.4-simple/*.yml ldv-linux-3.7.3/*.yml ldv-commit-tester/*.yml ldv-consumption/*.yml ldv-linux-3.12-rc1/*.yml ldv-linux-3.16-rc1/*.yml ldv-validator-v0.6/*.yml ldv-validator-v0.8/*.yml ldv-linux-4.2-rc1/*.yml ldv-linux-3.14/*.yml ldv-challenges/*.yml ldv-linux-4.0-rc1-mav/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64Large.set # ldv-challenges/linux-3.14_complex_emg_linux-alloc-spinlock_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-kernel-locking-mutex_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-sfc-sfc.cil.yml ldv-challenges/linux-3.14_complex_emg_linux-usb-dev_drivers-net-ethernet-sfc-sfc.cil.yml ldv-linux-3.14/linux-3.14_complex_emg_linux-drivers-clk1_drivers-net-ethernet-sfc-sfc.cil.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--gpu--drm--amd--amdgpu--amdgpu.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--gpu--drm--i915--i915.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--i915--i915.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.yml ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
SoftwareSystems-DeviceDriversLinux64-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set # ldv-linux-3.0/*.yml ldv-linux-3.4-simple/*.yml ldv-linux-3.7.3/*.yml ldv-commit-tester/*.yml ldv-consumption/*.yml ldv-linux-3.12-rc1/*.yml ldv-linux-3.16-rc1/*.yml ldv-validator-v0.6/*.yml ldv-validator-v0.8/*.yml ldv-linux-4.2-rc1/*.yml ldv-linux-3.14/*.yml ldv-challenges/*.yml ldv-linux-4.0-rc1-mav/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
SoftwareSystems-Other-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml
# sv-benchmarks/c/SoftwareSystems-BusyBox.set # busybox-1.22.0/*.yml
# sv-benchmarks/c/SoftwareSystems-OpenBSD.set # openbsd-6.2/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
SoftwareSystems-Other-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-BusyBox.set # busybox-1.22.0/*.yml
# sv-benchmarks/c/SoftwareSystems-OpenBSD.set # openbsd-6.2/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
SoftwareSystems-uthash-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-uthash.set # uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
SoftwareSystems-uthash-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-uthash.set # uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
SoftwareSystems-uthash-NoOverflows
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-uthash.set # uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
SoftwareSystems-uthash-MemCleanup
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-uthash.set # uthash-2.0.2/*.yml
with the specification:
CHECK( init(main()), LTL(G valid-memcleanup) )
SoftwareSystems-DeviceDriversLinux64-Termination
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set # ldv-linux-3.0/*.yml ldv-linux-3.4-simple/*.yml ldv-linux-3.7.3/*.yml ldv-commit-tester/*.yml ldv-consumption/*.yml ldv-linux-3.12-rc1/*.yml ldv-linux-3.16-rc1/*.yml ldv-validator-v0.6/*.yml ldv-validator-v0.8/*.yml ldv-linux-4.2-rc1/*.yml ldv-linux-3.14/*.yml ldv-challenges/*.yml ldv-linux-4.0-rc1-mav/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
SoftwareSystems-Intel-TDX-Module-ReachSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-Intel-TDX-Module.set # intel-tdx-module/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
7. ValidationCrafted
This category contains validation tasks that were crafted to test certain features of validators.
ValidationCraftedCorrectnessWitnesses-Loops
The verification tasks consist of the programs that match
# sv-benchmarks/c/CorrectnessWitnesses-Loops.set # loop-invariants64/witnesses/*.witness-validation.yml loop-invariants/witnesses/*.witness-validation.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )ValidationCrafted
ViolationWitnesses-ControlFlow
The verification tasks consist of the programs that match
# sv-benchmarks/c/ViolationWitnesses-ControlFlow.set # validation-crafted/witnesses/*.witness-validation.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
8. Overall
The category Overall contains all verification tasks of all above categories. Each above-mentioned main category is an own sub-category in category Overall. (The weighting schema is explained on the rules page.)
- ReachSafety
- MemSafety
- ConcurrencySafety
- NoOverflows
- Termination
- SoftwareSystems
- ValidationCrafted
9. FalsificationOverall
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.)
- ReachSafety
- MemSafety
- ConcurrencySafety
- NoOverflows
- SoftwareSystems
- ValidationCrafted
10. JavaOverall
ReachSafety-Java
The verification tasks consist of the programs that match
# sv-benchmarks/java/ReachSafety-Java.set # jayhorn-recursive/*.yml jbmc-regression/*.yml jpf-regression/*.yml java-ranger-regression/*.yml java-ranger-regression/WBS/*.yml java-ranger-regression/alarm/*.yml java-ranger-regression/infusion/*.yml java-ranger-regression/siena_eqchk/*.yml java-ranger-regression/replace5_eqchk/*.yml java-ranger-regression/nanoxml_eqchk/*.yml java-ranger-regression/printtokens_eqchk/*.yml MinePump/*.yml algorithms/*.yml juliet-java/*.yml jdart-regression/*.yml securibench/*.yml float-nonlinear-calculation/*.yml
with the specification:
CHECK( init(Main.main()), LTL(G assert) )
RuntimeException-Java
The verification tasks consist of the programs that match
# sv-benchmarks/java/ReachSafety-Java.set # jayhorn-recursive/*.yml jbmc-regression/*.yml jpf-regression/*.yml java-ranger-regression/*.yml java-ranger-regression/WBS/*.yml java-ranger-regression/alarm/*.yml java-ranger-regression/infusion/*.yml java-ranger-regression/siena_eqchk/*.yml java-ranger-regression/replace5_eqchk/*.yml java-ranger-regression/nanoxml_eqchk/*.yml java-ranger-regression/printtokens_eqchk/*.yml MinePump/*.yml algorithms/*.yml juliet-java/*.yml jdart-regression/*.yml securibench/*.yml float-nonlinear-calculation/*.yml
with the specification:
CHECK(init(Main.main()), LTL(G ! uncaught(java.lang.RuntimeException)))