Show simple item record

dc.contributor.authorBeyer, Dirk
dc.contributor.authorDangl, Matthias
dc.contributor.authorDietsch, Daniel
dc.contributor.authorHeizmann, Matthias
dc.contributor.authorStahlbauer, Andreas
dc.contributor.editorKnoop, Jens
dc.contributor.editorZdun, Uwe
dc.date.accessioned2017-06-21T07:37:23Z
dc.date.available2017-06-21T07:37:23Z
dc.date.issued2016
dc.identifier.isbn978-3-88579-646-6
dc.identifier.issn1617-5468
dc.description.abstractIt 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.en
dc.language.isoen
dc.publisherGesellschaft für Informatik e.V.
dc.relation.ispartofSoftware Engineering 2016
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Proceedings, Volume P-252
dc.titleVerification Witnessesen
dc.typeText/Conference Paper
dc.pubPlaceBonn
mci.reference.pages105-106
mci.conference.locationWien
mci.conference.date23.-26. Februar 2016


Files in this item

Thumbnail

Show simple item record