Verification Witnesses

Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, and Michael Tautschnig

Abstract

Over the last years, witness-based validation of verification results has become an established practice in software verification: An independent validator re-establishes verification results of a software verifier using verification witnesses, which are stored in a standardized exchange format. In addition to validation, such exchangable information about proofs and alarms found by a verifier can be shared across verification tools and users can apply independent third-party tools to visualize and explore witnesses to help them comprehend the causes of bugs or the reasons why a given program is correct. To achieve the goal of making verification results more accessible to engineers, it is necessary to consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the important principle of separation of concerns. We present the conceptual principles of verification witnesses, give a description how to use them, provide a technical specification of the exchange format for witnesses, and perform an extensive experimental study on the application of witness-based result validation, using the validators CPAchecker, Ultimate Automizer, CPA-witness2test, and FShell-witness2test.

Supplementary Data

We performed an extensive experimental evaluation to show the potential and feasibility of our approach. We used CPAchecker, CPA-witness2test, FShell-witness2test, and UltimateAutomizer to verify tasks from the SV-COMP 2019 benchmark set and applied both tools to validate their own witnesses. The following table provides links to the raw results of the experimental evaluation.

Category Verifier (Witness Producer) Witness Validator (Consumer)
Concurrency CPAchecker (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Ultimate Automizer (Results, Log files) CPAchecker (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
MemSafety CPAchecker (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Ultimate Automizer (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Overflows CPAchecker (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Ultimate Automizer (Results, Log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
ReachSafety CPAchecker (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
k‑Induction (Results, Log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Ultimate Automizer (Results, Log files) CPAchecker (Validation results, Validation log files, HTML table)
CPA-witness2test (Validation results, Validation log files, HTML table)
FShell-witness2test (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Termination CPAchecker (Results, Witnesses and log files) CPAchecker (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)
Ultimate Automizer (Results, Log files) CPAchecker (Validation results, Validation log files, HTML table)
Ultimate Automizer (Validation results, Validation log files, HTML table)

We used version 1.17 of BenchExec to run our experiments. The evaluated tools are available for download: