Verification Witnesses
dc.contributor.author | Beyer, D | |
dc.contributor.author | Dangl, M | |
dc.contributor.author | Dietsch, D | |
dc.contributor.author | Heizmann, M | |
dc.contributor.author | Lemberger, T | |
dc.contributor.author | Tautschnig, M | |
dc.date.accessioned | 2023-11-28T11:38:31Z | |
dc.date.available | 2023-11-28T11:38:31Z | |
dc.date.issued | 2022 | |
dc.identifier.issn | 1049-331X | |
dc.identifier.other | ARTN 57 | |
dc.identifier.other | ARTN 57 | |
dc.identifier.uri | https://qmro.qmul.ac.uk/xmlui/handle/123456789/92291 | |
dc.description.abstract | Over the last years, witness-based validation of verification results has become an established practice in software verification: An independent validator re-establishes verification results of a software verifier using verification witnesses, which are stored in a standardized exchange format. In addition to validation, such exchangable information about proofs and alarms found by a verifier can be shared across verification tools, and users can apply independent third-party tools to visualize and explore witnesses to help them comprehend the causes of bugs or the reasons why a given program is correct. To achieve the goal of making verification results more accessible to engineers, it is necessary to consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the important principle of separation of concerns. We present the conceptual principles of verification witnesses, give a description of how to use them, provide a technical specification of the exchange format for witnesses, and perform an extensive experimental study on the application of witness-based result validation, using the validators CPAchecker, UAutomizer, CPA-witness2test, and FShell-witness2test. | en_US |
dc.publisher | Association for Computing Machinery | en_US |
dc.relation.ispartof | ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY | |
dc.rights | This item is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. | |
dc.rights | Attribution 3.0 United States | * |
dc.rights.uri | http://creativecommons.org/licenses/by/3.0/us/ | * |
dc.subject | Violation witness | en_US |
dc.subject | correctness witness | en_US |
dc.subject | witness validation | en_US |
dc.subject | software verification | en_US |
dc.subject | program analysis | en_US |
dc.subject | model checking | en_US |
dc.subject | data-flow analysis | en_US |
dc.subject | formal methods | en_US |
dc.subject | certifying algorithm | en_US |
dc.title | Verification Witnesses | en_US |
dc.type | Article | en_US |
dc.rights.holder | © 2022 Copyright held by the owner/author(s). | |
dc.identifier.doi | 10.1145/3477579 | |
pubs.author-url | https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000859387700001&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=612ae0d773dcbdba3046f6df545e9f6a | en_US |
pubs.issue | 4 | en_US |
pubs.notes | Not known | en_US |
pubs.publication-status | Published | en_US |
pubs.volume | 31 | en_US |
rioxxterms.funder | Default funder | en_US |
rioxxterms.identifier.project | Default project | en_US |
Files in this item
This item appears in the following Collection(s)
Except where otherwise noted, this item's license is described as This item is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.