This repository describes the configuration of the competition machines (below) and the benchmark definition for each verifier (folder benchmark-defs/), in order to make results of the competition reproducible.
The competition uses several components to execute the benchmarks. The components are described in the following table.
Component | Repository | Participants |
---|---|---|
Verification Tasks | https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks | add, fix, review tasks |
Benchmark Definitions | https://gitlab.com/sosy-lab/sv-comp/bench-defs | define their parameters |
Tool-Info Modules | https://github.com/sosy-lab/benchexec/tree/main/benchexec/tools | define inferface |
Verifier Archives | https://gitlab.com/sosy-lab/sv-comp/archives-2023 | submit to participate |
Benchmarking Framework | https://github.com/sosy-lab/benchexec | (use to test their tool) |
Competition Scripts | https://gitlab.com/sosy-lab/benchmarking/competition-scripts | (use to reproduce) |
Witness Format | https://github.com/sosy-lab/sv-witnesses | (know) |
Task-Definition Format | https://gitlab.com/sosy-lab/benchmarking/task-definition-format | (know) |
Remote Execution | https://gitlab.com/sosy-lab/software/coveriteam | (use to test their tool) |
Archives published at Zenodo:
Concrete instructions on how to execute the experiments and to reproduce the results of the competition are available here: https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#instructions-for-execution-and-reproduction
A description of all installed Ubuntu packages, with their versions is given here: https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#installed-ubuntu-packages
SV-COMP provides a Docker image that tries to provide an environment that has mostly the same packages installed as the competition machines. The Docker image is described here: https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image
The parameters that are passed to the BenchExec [1] executor runexec on the competition machines are described here: https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#parameters-of-runexec
[1]: Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer (STTT), 21(1):1-29, 2019. https://doi.org/10.1007/s10009-017-0469-y