Show simple item record

dc.contributor.authorBeyer, Dirk
dc.contributor.authorDangl, Matthias
dc.contributor.authorDietsch, Daniel
dc.contributor.authorHeizmann, Matthias
dc.contributor.editorJürjens, Jan
dc.contributor.editorSchneider, Kurt
dc.date.accessioned2017-06-21T19:18:07Z
dc.date.available2017-06-21T19:18:07Z
dc.date.issued2017
dc.identifier.isbn978-3-88579-661-9
dc.identifier.issn1617-5468
dc.description.abstractStandard verification tools provide a counterexample to witness a specifica- tion violation. Since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the violation can be shared across verifiers and the user can use standard tools to visualize and explore witnesses. This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, users often struggle to comprehend why a program is correct, and there is no way to independently check the verification result. We recently closed this gap by complementing our earlier work on violation witnesses with correctness witnesses. The overall goal to make proofs avail- able to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago — our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the principle of separation of concerns. At any time, the correctness witness can be used to recon- struct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPACHECKER and ULTIMATEAUTOMIZER, to produce and validate witnesses.en
dc.language.isoen
dc.publisherGesellschaft für Informatik e.V.
dc.relation.ispartofSoftware Engineering 2017
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Proceedings, Volume P-267
dc.titleExchanging Verification Witnesses between Verifiersen
dc.typeText/Conference Paper
dc.pubPlaceBonn
mci.reference.pages93
mci.conference.sessiontitleVerification
mci.conference.locationHannover
mci.conference.date21.-24. Februar 2017


Files in this item

Thumbnail

Show simple item record