Name
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2786805.2786867 | Software Engineering |
Keywords | Field | DocType |
Error Witness, Counterexample Validation, Software Verification, Program Analysis, Model Checking | Programming language,Model checking,Computer science,Witness,Software,Counterexample,Program analysis,CPAchecker,State space,Software verification | Conference |
Citations | PageRank | References |
16 | 0.70 | 33 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dirk Beyer | 1 | 1736 | 100.85 |
| Matthias Dangl | 2 | 60 | 4.53 |
| Daniel Dietsch | 3 | 80 | 13.53 |
| Matthias Heizmann | 4 | 193 | 18.14 |
| Andreas Stahlbauer | 5 | 39 | 4.47 |