Witness Validation

URL

Change Log

When What
November 13th, 2015 Donated by Matthias Dangl

Reference

Studies who have been using the data (in any form) are required to include the following reference:

@inproceedings{Beyer:2015:WVS:2786805.2786867,
 author = {Beyer, Dirk and Dangl, Matthias and Dietsch, Daniel and Heizmann, Matthias and Stahlbauer, Andreas},
 title = {Witness Validation and Stepwise Testification Across Software Verifiers},
 booktitle = {Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering},
 series = {ESEC/FSE 2015},
 year = {2015},
 isbn = {978-1-4503-3675-8},
 location = {Bergamo, Italy},
 pages = {721--733},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2786805.2786867},
 doi = {10.1145/2786805.2786867},
 acmid = {2786867},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Counterexample Validation, Error Witness, Model Checking, Program Analysis, Software Verification},
}

About the Data

Paper Abstract

It is commonly understood that a verification tool should provide a counterexample to witness a specification violation. Until recently, software verifiers dumped error witnesses in proprietary formats, which are often neither human- nor machine-readable, and an exchange of witnesses between different verifiers was impossible. To close this gap in software-verification technology, we have defined an exchange format for error witnesses that is easy to write and read by verification tools (for further processing, e.g., witness validation) and that is easy to convert into visualizations that conveniently let developers inspect an error path. To eliminate manual inspection of false alarms, we develop the notion of stepwise testification: in a first step, a verifier finds a problematic program path and, in addition to the verification result FALSE, constructs a witness for this path; in the next step, another verifier re-verifies that the witness indeed violates the specification. This process can have more than two steps, each reducing the state space around the error path, making it easier to validate the witness in a later step. An obvious application for testification is the setting where we have two verifiers: one that is efficient but imprecise and another one that is precise but expensive. We have implemented the technique of error-witness-driven program analysis in two state-of-the-art verification tools, CPAchecker and Ultimate Automizer, and show by experimental evaluation that the approach is applicable to a large set of verification tasks.