Violation Witnesses and Result Validation
for Multi-Threaded Programs

Implementation and Evaluation with CPAchecker

Dirk Beyer and Karlheinz Friedberger


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

How to reproduce the results

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.