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

D 2022

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

BEYER, Dirk a Jan STREJČEK

Základní údaje

Originální název

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

Autoři

BEYER, Dirk (276 Německo) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings, od s. 160-174, 15 s. 2022

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/22:00127777

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-22307-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-031-22308-2_8

UT WoS

000916500200008

Klíčová slova anglicky

software verification;program analysis;software validation;software bugs;verification witnesses;evaluation;benchmarking

Štítky

core_B, firank_B, formal verification, formela-conference, formela-ver, program analysis, verification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 3. 2023 12:08, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

BEYER, Dirk a Jan STREJČEK. Case Study on Verification-Witness Validators: Where We Are and Where We Go. Online. In Gagandeep Singh, Caterina Urban. Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings. Cham (Switzerland): Springer, 2022, s. 160-174. ISBN 978-3-031-22307-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-22308-2_8.

@inproceedings{2244108,
   author = {Beyer, Dirk and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-031-22308-2_8},
   editor = {Gagandeep Singh, Caterina Urban},
   keywords = {software verification;program analysis;software validation;software bugs;verification witnesses;evaluation;benchmarking},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-031-22307-5},
   pages = {160-174},
   publisher = {Springer},
   title = {Case Study on Verification-Witness Validators: Where We Are and Where We Go},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-22308-2_8},
   year = {2022}
}

TY  - JOUR
ID  - 2244108
AU  - Beyer, Dirk - Strejček, Jan
PY  - 2022
TI  - Case Study on Verification-Witness Validators: Where We Are and Where We Go
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783031223075
KW  - software verification;program analysis;software validation;software bugs;verification witnesses;evaluation;benchmarking
UR  - https://link.springer.com/chapter/10.1007/978-3-031-22308-2_8
N2  - 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.
ER  -

BEYER, Dirk a Jan STREJČEK. Case Study on Verification-Witness Validators: Where We Are and Where We Go. Online. In Gagandeep Singh, Caterina Urban. \textit{Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings}. Cham (Switzerland): Springer, 2022, s.~160-174. ISBN~978-3-031-22307-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-22308-2\_{}8.

Podrobný výpis o publikaci