Invariants and error traces are an important outcome of a program analysis, and therefore, a standardized exchange format for verification witnesses is used by many program analyzers. This way, information about program traces and variable assignments can be shared across tools, e.g., to validate verification results, or provided to users, e.g., to visualize and explore the results in order to fix bugs or understand the reason for a program's correctness. The standard format for correctness and violation witnesses that was used by SV-COMP for several years was only applicable to sequential (single-threaded) programs. For validating multi-threaded programs, we extend the existing standard exchange format by adding information about thread management and thread interleaving. We contribute a reference implementation of a validator for violation witnesses in the new format, which we implemented as component of the software-verification framework CPAchecker. We experimentally evaluate the format and validator on a large set of violation witnesses. The outcome is promising: several verification tools already produce violation witnesses that help validating the verification result, and our witness validator can re-verify most of the produced witnesses.
The supplementary archive contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker and other tools. Next to a README, the supplementary archive contains the necessary tools and our experimental results
./benchmark-defs/The input files for the benchmarking script.
./results-verified/Our raw results from the verification process of verification tools that produce violation witnesses for multi-threaded programs, including log files and witness files.
./results-validated/Our raw results from the validation process of our validator CPAchecker, applied for the violation witnesses from
./results-verified/, including log files.
./sv-benchmarks/Multi-threaded tasks copied from the SV-Benchmark repository.
./tools/This directory contains the executed tools. We include CPAchecker as a ready-to-run application and provide a script to automatically download other tools from the SV-COMP20 archive.
In order to reproduce the results, download the supplementary archive. Please follow the README file in the archive to install further tools and perform the evaluation.