Supplementary Web Page for SAS 2022 Article ’Case Study on Verification-Witness Validators: Where We Are and Where We Go’

Dirk Beyer and Jan Strejček
LMU Munich, Munich, Germany and Masaryk University, Brno, Czechia
Abstract. 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.

Keywords: Software verification · Program analysis · Software validation · Software bugs · Verification witnesses · Evaluation · Benchmarking

Table 1: Validation of violation witnesses by eight violation validators; the numbers are hyperlinked to the tables generated by BenchExec
Category Witnesses CPAchecker CPA-w2t CProver-w2t Dartgnan MetaVal nitwit Symbiotic
-Witch
UAutomizer
ReachSafety
valid 26797 14908 8628 14168 0 15507 11176 8592
invalid 5 177 28 12 2 0 10 0 0
MemSafety
valid 16984 12594 231 954 116 8394 4197
invalid 2 804 0 0 26 2 0 0
ConcurrencySafety
valid 4746 2700 1464
invalid 1293 40 0
NoOverflows
valid 2808 2334 887 1436 1982 2609 2468
invalid 167 0 0 0 0 0 0
Termination
valid 3652 2580 598 960
invalid 56 21 0 0
SoftwareSystems
valid 2102 621 6 33 0 0 179 26
invalid 5903 5 0 27 0 0 51 4

Table 2: Validation of correctness witnesses by three correctness validators; the numbers are hyperlinked to the tables generated by BenchExec
Category Witnesses CPAchecker MetaVal UAutomizer
ReachSafety
valid 31013 17312 19655 19632
invalid 894 0 315 3
MemSafety
valid 16948 227 14384
invalid 326 0 0
ConcurrencySafety
valid 3177
invalid 389
NoOverflows
valid 2089 1718 1608 1713
invalid 300 0 36 0
Termination
valid 4502
invalid 14
SoftwareSystems
valid 25819 6771 20624 19343
invalid 888 0 403 0