Benchmark Verification Tasks
All verification tasks are available for web browsing and for download via the following Git repository (for SV-COMP 2026 visit the tag 'svcomp26'): 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.
The following figures show the category structure of normal categories (Fig. 1) and sponsored categories (Fig. 2) in SV-COMP 2026.
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. C.ReachSafety
C.unreach-call.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())) )
C.unreach-call.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())) )
C.unreach-call.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())) )
C.unreach-call.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 infeasible-control-flow/*.yml
# sv-benchmarks/c/Sanity.set # nondet-memory-examples/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.unreach-call.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())) )
C.unreach-call.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())) )
C.unreach-call.Hardness
The verification tasks consist of the programs that match
# sv-benchmarks/c/Hardness.set # hardness/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.unreach-call.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())) )
C.unreach-call.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-cve/*.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())) )
C.unreach-call.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 verifythis/linked-list-removal.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.unreach-call.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())) )
C.unreach-call.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 fuzzle-programs/*.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())) )
C.unreach-call.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())) )
C.unreach-call.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())) )
2. C.MemSafety
C.valid-memcleanup.Main
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-cve/*.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 verifythis/linked-list-removal.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) )
C.valid-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 verifythis/linked-list-removal.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) )
C.valid-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-cve/*.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) )
C.valid-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) )
C.valid-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) )
C.valid-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 infeasible-control-flow/*.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 fuzzle-programs/*.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) )
3. C.Concurrency
C.no-data-race.Concurrency
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) )
C.no-overflow.Concurrency
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) )
C.unreach-call.Concurrency
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())) )
C.valid-memsafety.Concurrency
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) )
4. C.NoOverflows
C.no-overflow.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) )
C.no-overflow.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 infeasible-control-flow/*.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-cve/*.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 fuzzle-programs/*.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 verifythis/linked-list-removal.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) )
5. C.Termination
C.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) )
C.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) )
C.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) )
C.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 infeasible-control-flow/*.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-cve/*.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 fuzzle-programs/*.yml
# sv-benchmarks/c/Sequentialized.set # systemc/*.yml seq-mthreaded/*.yml seq-mthreaded-reduced/*.yml seq-pthread/*.yml
with the specification:
CHECK( init(main()), LTL(F end) )
6. C.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.
C.no-overflow.SoftwareSystems-BusyBox
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) )
C.no-overflow.SoftwareSystems-coreutils
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml coreutils-v9.5-units/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
C.no-overflow.SoftwareSystems-uthash
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) )
C.termination.SoftwareSystems-DeviceDriversLinux64
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) )
C.termination.SoftwareSystems-uthash
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(F end) )
C.unreach-call.SoftwareSystems-AWS-C-Common
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())) )
C.unreach-call.SoftwareSystems-DeviceDriversLinux64
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())) )
C.unreach-call.SoftwareSystems-DeviceDriversLinux64Large
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())) )
C.unreach-call.SoftwareSystems-Intel-TDX-Module
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())) )
C.unreach-call.SoftwareSystems-Other
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml coreutils-v9.5-units/*.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())) )
C.unreach-call.SoftwareSystems-uthash
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())) )
C.valid-memcleanup.SoftwareSystems-uthash
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) )
C.valid-memsafety.SoftwareSystems-coreutils
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-coreutils.set # goblint-coreutils/*.yml coreutils-v8.31/*.yml coreutils-v9.5-units/*.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) )
C.valid-memsafety.SoftwareSystems-DeviceDriversLinux64
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) )
C.valid-memsafety.SoftwareSystems-Other
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) )
C.valid-memsafety.SoftwareSystems-uthash
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) )
7. C.ValidationCrafted
This category contains validation tasks that were crafted to test certain features of validators.
C.unreach-call.CorrectnessWitnesses
The verification tasks consist of the programs that match
# sv-benchmarks/c/CorrectnessWitnesses.set # loop-invariants64/witnesses/*.witness-validation.yml loop-invariants/witnesses/*.witness-validation.yml loop-lit/witnesses/*.witness-validation.yml loops/witnesses/*.witness-validation.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.unreach-call.ViolationWitnesses
The verification tasks consist of the programs that match
# sv-benchmarks/c/ViolationWitnesses.set # validation-crafted/witnesses/*.witness-validation.yml termination-restricted-15/witnesses/*.witness-validation.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.termination.ViolationWitnesses
The verification tasks consist of the programs that match
# sv-benchmarks/c/ViolationWitnesses.set # validation-crafted/witnesses/*.witness-validation.yml termination-restricted-15/witnesses/*.witness-validation.yml
with the specification:
CHECK( init(main()), LTL(F end) )
8. C.Overall
The category C.Overall contains all verification tasks of all above categories. Each above-mentioned main category is an own sub-category in category C.Overall. (The weighting schema is explained on the rules page.)
- C.ReachSafety
- C.MemSafety
- C.Concurrency
- C.NoOverflows
- C.Termination
- C.SoftwareSystems
- C.ValidationCrafted
9. C.FalseOverall
The category C.FalseOverall consists of all verification tasks and the results "correct TRUE" and "incorrect TRUE" are not counted. (The weighting schema is the same as for C.Overall.)
- C.ReachSafety
- C.MemSafety
- C.Concurrency
- C.NoOverflows
- C.Termination
- C.SoftwareSystems
10. C.TrueOverall
The category C.TrueOverall consists of all verification tasks and the results "correct FALSE" and "incorrect FALSE" are not counted. (The weighting schema is the same as for C.Overall.)
- C.ReachSafety
- C.MemSafety
- C.Concurrency
- C.NoOverflows
- C.Termination
- C.SoftwareSystems
11. C.Huawei-Concurrency-Challenges
C.no-data-race.Huawei-Concurrency-Challenges
The verification tasks consist of the programs that match
# sv-benchmarks/c/Huawei-Concurrency-Challenges.set # libvsync/*.yml pthread-complex/*.yml
with the specification:
CHECK( init(main()), LTL(G ! data-race) )
C.no-overflow.Huawei-Concurrency-Challenges
The verification tasks consist of the programs that match
# sv-benchmarks/c/Huawei-Concurrency-Challenges.set # libvsync/*.yml pthread-complex/*.yml
with the specification:
CHECK( init(main()), LTL(G ! overflow) )
C.unreach-call.Huawei-Concurrency-Challenges
The verification tasks consist of the programs that match
# sv-benchmarks/c/Huawei-Concurrency-Challenges.set # libvsync/*.yml pthread-complex/*.yml
with the specification:
CHECK( init(main()), LTL(G ! call(reach_error())) )
C.valid-memsafety.Huawei-Concurrency-Challenges
The verification tasks consist of the programs that match
# sv-benchmarks/c/Huawei-Concurrency-Challenges.set # libvsync/*.yml pthread-complex/*.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) )
12. Java.Overall
Java.no-runtime-exception.Main
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_unboundedloop/*.yml float-nonlinear-calculation/*.yml argv-tasks/*.yml autostub/*.yml objects/*.yml
with the specification:
CHECK(init(Main.main()), LTL(G ! uncaught(java.lang.RuntimeException)))
Java.valid-assert.Main
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_unboundedloop/*.yml float-nonlinear-calculation/*.yml argv-tasks/*.yml autostub/*.yml objects/*.yml
with the specification:
CHECK( init(Main.main()), LTL(G assert) )
13. SV-LIB.Overall
SV-LIB.correct-tags.CoreVerification
The verification tasks consist of the programs that match
# sv-benchmarks/sv-lib/CoreVerification.set # core-verification/*.yml
SV-LIB.correct-tags.CoreValidation
The verification tasks consist of the programs that match
# sv-benchmarks/sv-lib/CoreValidation.set # core-validation/*.yml
SV-LIB.correct-tags.CTranslated
The verification tasks consist of the programs that match
# sv-benchmarks/sv-lib/CTranslated.set # c-translated/**/*.yml