Case Study on Verification-Witness Validators: Where We Are and Where We Go

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00127777" target="_blank" >RIV/00216224:14330/22:00127777 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007/978-3-031-22308-2_8" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-22308-2_8</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-22308-2_8" target="_blank" >10.1007/978-3-031-22308-2_8</a>

Result language
angličtina
Original language name
Case Study on Verification-Witness Validators: Where We Are and Where We Go
Original language description
Software-verification tools sometimes produce incorrect answers, which can be a false alarm or a wrong claim of correctness. To increase the reliability of verification results, many verifiers now accompany their answers by witnesses in an interoperable standard format. There exist witness validators that can examine the witnesses and potentially confirm the verification results. This case study analyzes the quality of existing witness validators for C programs using the witnesses produced by a wide variety of 40 verification tools that participated in SV-COMP 2022. In particular, we show that many witness validators sometimes confirm witnesses that are invalid. To remedy this situation, we suggest some advances in witness validation, including a regular comparative evaluation of validators. Our suggestions were recently adopted by the SV-COMP community for the next edition of the competition.
Czech name
—
Czech description
—

Project
—
Continuities
S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings
ISBN
9783031223075
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
160-174
Publisher name
Springer
Place of publication
Cham (Switzerland)
Event location
Auckland
Event date
Jan 1, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000916500200008

Similar results(10)