Benchmark Test Tasks
All test tasks are available for web browsing and for download via the following Git repository (for Test-Comp 2025 visit the tag 'testcomp25'): https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
This edition of the competition on software testing is based on the following categories of test tasks. The test tasks are taken from the most diverse and publicly available repository of tasks, which were collected and contributed by the community on software verification.
For illustration, the structured overview
from the competition report shows the categories.
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/test-comp/bench-defs).
1. Cover-Error
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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
ReachSafety-XCSP
The verification tasks consist of the programs that match
# sv-benchmarks/c/XCSP.set # xcsp/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@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:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
SoftwareSystems-BusyBox-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-BusyBox.set # busybox-1.22.0/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
SoftwareSystems-coreutils
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:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
SoftwareSystems-OpenBSD-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-OpenBSD.set # openbsd-6.2/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
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:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
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:
COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) )
2. Cover-Branches
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
ReachSafety-Fuzzle
The verification tasks consist of the programs that match
# sv-benchmarks/c/Fuzzle.set # fuzzle-programs/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
ReachSafety-Hardness
The verification tasks consist of the programs that match
# sv-benchmarks/c/Hardness.set # hardness-nfm22/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
ReachSafety-ProductLines
The verification tasks consist of the programs that match
# sv-benchmarks/c/ProductLines.set # product-lines/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
ReachSafety-XCSP
The verification tasks consist of the programs that match
# sv-benchmarks/c/XCSP.set # xcsp/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
ReachSafety-Combinations
The verification tasks consist of the programs that match
# sv-benchmarks/c/Combinations.set # combinations/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
SoftwareSystems-BusyBox-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-BusyBox.set # busybox-1.22.0/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
SoftwareSystems-coreutils
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
SoftwareSystems-OpenBSD-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-OpenBSD.set # openbsd-6.2/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
SoftwareSystems-SQLite-MemSafety
The verification tasks consist of the programs that match
# sv-benchmarks/c/SoftwareSystems-SQLite.set # sqlite/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
Termination-BitVectors
The verification tasks consist of the programs that match
# sv-benchmarks/c/BitVectors-Termination.set # termination-bwb/*.yml
with the specification:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
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:
COVER( init(main()), FQL(COVER EDGES(@DECISIONEDGE)) )
3. Overall
- Cover-Error
- Cover-Branches