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