Case Study on Verification-Witness Validators: Where We Are and Where We Go
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 format. There are witness validators that can examine the witnesses and potentially confirm the verification results. This case study analyses the quality of existing witness validators for C programs using the witnesses produced by a wide variety of 47 verification tools that participated in SV-COMP 2022. In particular, we study the amount of cases in which a witness validator confirms an incorrect witness. We also suggest some advances in witness validation, including a scoring for a comparative evaluation of validators. These suggestions were recently approved by the SV-COMP community.
Mon 5 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mTalk | Parameterized Recursive Refinement Types for Automated Program Verification SAS Ryoya Mukai The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan | ||
11:00 30mTalk | Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual SAS Isabel Garcia-Contreras University of Waterloo, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, inc. | ||
11:30 30mTalk | Case Study on Verification-Witness Validators: Where We Are and Where We Go SAS Link to publication DOI Media Attached | ||