Benchmark Set with Useful Witnesses. In order to provide meaningful results, we need to assemble an appropriate benchmark set consisting of witnesses that indeed contain useful information, i.e., information that potentially improves the results of another tool. As a starting point, we consider correctness witnesses from the final runs of SV-COMP 2022 [8, 10]. This means that for one verification task we might get multiple correctness witnesses (from different participating verifiers), while for others we might even get none because no verifier was able to come up with a proof. We select the witnesses for tasks in the subcategory ReachSafety-Loops, because this subcategory is focussed on verifying programs with challenging loop invariants. This selection leaves us with 6242 correctness witnesses (without knowing which of those actually contain useful information). For each of the selected witnesses we converted the contained invariants into both ACSL annotations (for verification with Frama-C) and assertions (for verifi- cation with automatic verifiers from SV-COMP 2022). Here we can immediately drop those witnesses that do not result in any annotations being generated, which results in 1931 witnesses belonging to 640 different verification tasks. 2 xxxxx://xxxxxx.xxx/sosy-lab/sv-comp/archives-2022/-/tree/svcomp22/2022 Table 1: Impact of cooperation: in each row, a ‘consuming’ verifier is fed with information from witnesses of our benchmark set; ‘Baseline’ reports the number of programs that the verifier proved correct without any help; ‘Improved via coop.’ reports the number of programs that the verifier can prove in addition, if the information from the witness is provided Consuming verifier Benchmark tasks (434 total) Projection on programs (230 total) Baseline Improved via coop. Baseline Improved via coop. 2ls 157 179 83 111 UAutomizer 360 47 186 31 Cbmc 281 53 142 28 CPAchecker 300 69 149 53 Dartagnan 280 82 139 51 Esbmc 000 000 000 76 gazer-theta 266 118 135 64 Goblint 38 106 21 47 UKojak 191 134 97 76 Korn 183 46 98 27 PeSCo 180 162 87 99 Pinaka 000 000 000 59 Symbiotic 349 51 174 32 Utaipan 334 65 172 37 VeriAbs 343 31 186 28 Frama-C 211 31 105 20 We then run each verifier for each program where annotations have been generated, once with the original, unmodified program, and n times with the transformed program for each of the n witnesses. This allows us determine whether any improvement was achieved, by looking at the differences between verification of the unmodified program versus ...
