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 and Jan STREJČEK

Basic information

Original name

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

Authors

BEYER, Dirk (276 Germany) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/22:00127777

Organization unit

Faculty of Informatics

ISBN

978-3-031-22307-5

ISSN

DOI

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

UT WoS

000916500200008

Keywords in English

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

Abstract

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 and 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, p. 160-174. ISBN 978-3-031-22307-5. Available from: 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 and 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, p.~160-174. ISBN~978-3-031-22307-5. Available from: https://dx.doi.org/10.1007/978-3-031-22308-2\_{}8.

Detailed Information on Publication Record