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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

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

Rok uplatnění

2022

Kód důvěrnosti údajů

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

Název statě ve sborníku

Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings

ISBN

9783031223075

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

160-174

Název nakladatele

Springer

Místo vydání

Cham (Switzerland)

Místo konání akce

Auckland

Datum konání akce

1. 1. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000916500200008