Verification Witnesses

Abstract

It is commonly understood that a verification tool should provide a counterex-ample to witness a specification violation. Until recently, software verifiers dumped error witnesses in proprietary formats, which are often neither humannor machine-readable, and an exchange of witnesses between different verifiers was impossible. 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). 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. The technique of error-witness-driven program analysis is implemented in two state-of-the-art verification tools, CPACHECKER and ULTIMATE AUTOMIZER.