---

Abstract

Traditionally, a verification task is considered solved as soon as a property violation or a correctness proof is found. In practice, this is where the actual work starts: Is it just a false alarm? Is the error reproducible? Can the error report later be re-used for bug fixing or regression testing? The advent of exchangeable witnesses is a paradigm shift in verification, from simple answers true and false towards qualitatively more valuable information about the reason for the property violation. This paper explains a convenient web-based toolchain that can be used to answer the above questions. We consider as example application the verification of C programs. Our first component collects witnesses and stores them for later re-use; for example, if the bug is fixed, the witness can be tried once again and should now be rejected, or, if the bug was not scheduled for fixing, the database can later provide the witnesses in case an engineer wants to start fixing the bug. Our second component is a web service that takes as input a witness for the property violation and (re-)validates it, i.e., it re-plays the witness on the system in order to re-explore the state-space in question. The third component is a web service that continues from the second step by offering an interactive visualization that interconnects the error path, the system's sources, the values on the path (test vectors), and the reachability graph. We evaluated the feasibility of our approach on a large benchmark of verification tasks.

Demo

We invite you to try out our tool chain.

• We provide an archive of example interactive reports.
• We provide a supplementary virtual machine image set up for producing witnesses by verifying tasks using CPAchecker and producing interactive reports for validating witnesses with CPAchecker. The virtual machine also contains the example reports.
• Finally, we also provide access to our web service instance.
Note that the web service provides a live view on data produced by experiments conducted in our lab, so that you may encounter witnesses for false alarms, which will not be accepted by the validator, which will therefore only provide a report documenting the failed validation instead of an interactive error report.