Demonstrations of witness visualization using the Witness Visualizer Tool

<p>We have three datasets that display visualized <a href="https://sv-comp.sosy-lab.org/">SVCOMP</a> witnesses generated with the help of the <a href="https://github.com/ispras/cv">Witness Visualizer tool</a>. Each dataset comprises two directories:&nbsp;<code>witnesses</code>, which contains the original witnesses provided by SVCOMP tools, and <code>visualization</code>, which contains our visual representations of the respective witnesses in HTML format. The visualization file name contains the prefix <code>error_trace-</code>, for example, <code>error_trace-witness.2ls.html</code> corresponds to a witness named <code>witness.2ls.graphml</code>.</p> <h3>1. Overall thoroughness for all SVCOMP tools (<a href="../records/10988025/files/dataset_1.zip?download=1" target="_blank" rel="noopener">dataset_1.zip</a>)</h3> <p>This dataset includes a single random witness for each SVCOMP tool, accompanied by its corresponding visualization. The visualizations showcase the various witness elements such as function calls, conditions, assumptions, thread specifics, and other operations. Cells marked with <code>+/-</code> indicate that some elements were present in the error trace, but not all of them. All witnesses are presented in the table below:</p> <table> <tbody> <tr> <td>Witness</td> <td>SV-COMP Tool</td> <td>Function calls</td> <td>Threads</td> <td>Assumptions</td> <td>Conditions</td> <td>Link to sources</td> </tr> <tr> <td>witness.2ls.graphml</td> <td>2LS</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.aprove.graphml</td> <td>AProVE (2022)</td> <td>-</td> <td>-</td> <td>-</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.brick.graphml</td> <td>BRICK</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.bubaak.graphml</td> <td>Bubaak</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.cbmc.graphml</td> <td>CBMC</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.cpa-bam-bnb.graphml</td> <td>CPA-BAM-BnB</td> <td>+</td> <td>-</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.cpa-bam-smg.graphml</td> <td>CPA-BAM-SMG</td> <td>+</td> <td>-</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.cpalockator.graphml</td> <td>CPALockator</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.cpachecker.graphml</td> <td>CPAChecker</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.crux.graphml</td> <td>Crux</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.cseq.graphml</td> <td>Cseq</td> <td>+</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.dartagnan.graphml</td> <td>Dartagnan</td> <td>-</td> <td>+</td> <td>-</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.deagle.graphml</td> <td>Deagle</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>-</td> <td>DIVINE (until 2022)</td> <td>empty</td> </tr> <tr> <td>-</td> <td>EBF</td> <td>empty</td> </tr> <tr> <td>witness.esbmc-incr.graphml</td> <td>ESBMC-incr</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.esbmc-kind.graphml</td> <td>ESBMC-kind</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>-</td> <td>Frama-C-SV</td> <td>empty</td> </tr> <tr> <td>witness.gazer-theta.graphml</td> <td>Gazer-Theta</td> <td>+</td> <td>-</td> <td>+</td> <td>-</td> <td>wrong path</td> </tr> <tr> <td>witness.gdart.graphml</td> <td>Gdart-LLVM</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>-</td> <td>Goblint</td> <td>empty</td> </tr> <tr> <td>witness.graves_cpa.graphml</td> <td>Graves-CPA</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.graves_par.graphml</td> <td>Graves-Par</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>-</td> <td>Infer</td> <td>empty</td> </tr> <tr> <td>witness.korn.graphml</td> <td>Korn</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.lart.graphml</td> <td>LART (2022)</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.lazy-cseq.graphml</td> <td>Lazy-CSeq</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.lfchecker.graphml</td> <td>LF-checker</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>-</td> <td>Locksmith</td> <td>empty</td> </tr> <tr> <td>-</td> <td>Mopsa</td> <td>empty</td> </tr> <tr> <td>witness.pesco_cpa.graphml</td> <td>PeSCo-CPA</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.pichecker.graphml</td> <td>PIChecker</td> <td>+</td> <td>-</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.pinaka.graphml</td> <td>Pinaka</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.predator.graphml</td> <td>PredatorHP</td> <td>-</td> <td>-</td> <td>-</td> <td>-</td> <td>+</td> </tr> <tr> <td>-</td> <td>SESL (2022)</td> <td>empty</td> </tr> <tr> <td>witness.smack.graphml</td> <td>SMACK (until 2022)</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.symbiotic.graphml</td> <td>Symbiotic</td> <td>-</td> <td>+</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.theta.graphml</td> <td>Theta</td> <td>different format</td> </tr> <tr> <td>witness.uatomozer.graphml</td> <td>UAutomizer</td> <td>+/-</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.ucutter.graphml</td> <td>UgemCutter</td> <td>+/-</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.ukojak.graphml</td> <td>UKojak</td> <td>+/-</td> <td>-</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.utaipan.graphml</td> <td>UTaipan</td> <td>+/-</td> <td>+</td> <td>+</td> <td>+</td> <td>+</td> </tr> <tr> <td>witness.veriabs.graphml</td> <td>VeriAbs</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>wrong path</td> </tr> <tr> <td>witness.veriabsl.graphml</td> <td>VeriAbsL</td> <td>+</td> <td>-</td> <td>+</td> <td>+</td> <td>wrong path</td> </tr> <tr> <td>witness.verifuzz.graphml</td> <td>VeriFuzz</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> <tr> <td>witness.verioover.graphml</td> <td>VeriOover</td> <td>-</td> <td>-</td> <td>+</td> <td>-</td> <td>+</td> </tr> </tbody> </table> <h3>2. Thoroughness by property (<a href="../records/10988025/files/dataset_2.zip?download=1" target="_blank" rel="noopener">dataset_2.zip</a>)</h3> <p>This dataset comprises a selected witness for each SVCOMP property (ReachSafety, MemSafety, Termination, NoOverflow, ConcurrencySafety). The witnesses are presented in the following table:</p> <p>&nbsp;</p> <table> <tbody> <tr> <td>Witness</td> <td>SV-COMP Tool</td> <td>Property</td> <td>Mandatory elements</td> <td>Description</td> </tr> <tr> <td>witness.smg_memory.graphml</td> <td>CPA-BAM-SMG</td> <td>MemSafety</td> <td>Assumptions / conditions, function calls</td> <td>There is a double free operation. Employing function calls <code>append </code>aids in comprehending the structure of the list, while assumptions reveal which branch was chosen.</td> </tr> <tr> <td>witness.graves_overflow.graphml</td> <td>Graves-CPA</td> <td>NoOverflow</td> <td>Assumptions / conditions</td> <td>The witness showcases an explicit (<code>-2147483648</code>, which represents the minimal value for the <code>int</code>&nbsp;type), which has the potential to cause overflow in specific program.</td> </tr> <tr> <td>witness.cpachecker_termination.graphml</td> <td>CPAChecker</td> <td>NoTermination</td> <td>Assumptions / conditions</td> <td>There is a condition leading to an infinite loop.</td> </tr> <tr> <td>witness.cpachecker_unreach.graphml</td> <td>CPAChecker</td> <td>ReachSafety</td> <td>Function calls</td> <td>The error trace indicates a potential scenario where a <code>mutex</code> was unlocked<br>without the corresponding <code>mutex_unlock</code> operation.</td> </tr> <tr> <td>witness.cpachecker_conc.graphml</td> <td>CPAChecker</td> <td>ConcurrencySafety</td> <td>Function calls, thread operations</td> <td>The error trace illustrates the creation of threads and highlights the assignments made within each thread that ultimately resulted in the violation of the property.</td> </tr> </tbody> </table> <div> <h3>3. Known bug (<a href="../records/10988025/files/dataset_2.zip?download=1" target="_blank" rel="noopener">dataset_3.zip</a>)</h3> <p>This dataset contains witnesses for a known bug from SVCOMP (<code>linux-3.14--drivers--usb--misc--adutux.ko.cil.i</code>) involving a data race on <code>dev-&gt;udev</code>, where concurrent writes occur without corresponding locks. Only two tools were able to solve the corresponding verification task: ESBMC-kind and CPALockator. The ESBMC error trace (<code>witness.esbmc_2020.graphml</code>) includes only thread specifics and assumptions, while the CPALockator witness (<code>witness.lockator.graphml</code>) comprises all witness elements and is presented in a human-readable format.</p> <h3>4. Comparison with the validation rate</h3> <p>This section presents a comparison between witness thoroughness and the actual validation rate for each property. We considered all tools that participated in the respective category and generated at least 10 error traces, then calculated the validation rate. This comparison demonstrates how effectively thoroughness can approximate the validation rate. The following tables provide details for each property, with the relevant elements used to calculate thoroughness highlighted:</p> <ul> <li>MemSafety property:</li> </ul> <table> <tbody> <tr> <td>SV-COMP Tool</td> <td><strong>Function calls</strong></td> <td>Threads</td> <td><strong>Assumptions</strong></td> <td><strong>Conditions</strong></td> <td>Thoroughness</td> <td>Error traces</td> <td>Validation rate</td> </tr> <tr> <td>Bubaak</td> <td><strong>0</strong></td> <td>0</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>33.33</td> <td>64</td> <td>67.19</td> </tr> <tr> <td>CBMC</td> <td><strong>0</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>33.33</td> <td>27</td> <td>11.11</td> </tr> <tr> <td>CPA-BAM-SMG</td> <td><strong>1</strong></td> <td>0</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>46</td> <td>78.26</td> </tr> <tr> <td>CPAChecker</td> <td><strong>1</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>37</td> <td>67.57</td> </tr> <tr> <td>ESBMC-kind</td> <td><strong>0</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>33.33</td> <td>25</td> <td>20</td> </tr> <tr> <td>Graves-CPA</td> <td><strong>1</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>44</td> <td>56.82</td> </tr> <tr> <td>Graves-Par</td> <td><strong>1</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>18</td> <td>77.78</td> </tr> <tr> <td>PeSCo-CPA</td> <td><strong>1</strong></td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>37</td> <td>67.57</td> </tr> </tbody> </table> <ul> <li>NoOverflow property:</li> </ul> <table> <tbody> <tr> <td>SV-COMP Tool</td> <td>Function calls</td> <td>Threads</td> <td><strong>Assumptions</strong></td> <td>Conditions</td> <td>Thoroughness</td> <td>Error traces</td> <td>Validation rate</td> </tr> <tr> <td>2LS</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>2071</td> <td>95.7</td> </tr> <tr> <td>Bubaak</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>2233</td> <td>94.67</td> </tr> <tr> <td>CBMC</td> <td>0</td> <td>1</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>3296</td> <td>62.14</td> </tr> <tr> <td>CPAChecker</td> <td>1</td> <td>1</td> <td><strong>1</strong></td> <td>1</td> <td>100</td> <td>196</td> <td>100</td> </tr> <tr> <td>Crux</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>222</td> <td>95.05</td> </tr> <tr> <td>ESBMC-kind</td> <td>0</td> <td>1</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>3296</td> <td>66.69</td> </tr> <tr> <td>Frama-C-SV</td> <td>0</td> <td>0</td> <td><strong>0</strong></td> <td>0</td> <td>0</td> <td>676</td> <td>0</td> </tr> <tr> <td>Graves-Par</td> <td>1</td> <td>1</td> <td><strong>1</strong></td> <td>1</td> <td>100</td> <td>750</td> <td>2</td> </tr> <tr> <td>Infer</td> <td>0</td> <td>0</td> <td><strong>0</strong></td> <td>0</td> <td>0</td> <td>583</td> <td>0</td> </tr> <tr> <td>Pinaka</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>2232</td> <td>100</td> </tr> <tr> <td>Symbiotic</td> <td>0</td> <td>1</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>1418</td> <td>100</td> </tr> <tr> <td>UAutomizer</td> <td>0.5</td> <td>1</td> <td><strong>1</strong></td> <td>1</td> <td>100</td> <td>2222</td> <td>100</td> </tr> <tr> <td>UKojak</td> <td>0.5</td> <td>0</td> <td><strong>1</strong></td> <td>1</td> <td>100</td> <td>168</td> <td>100</td> </tr> <tr> <td>UTaipan</td> <td>0.5</td> <td>1</td> <td><strong>1</strong></td> <td>1</td> <td>100</td> <td>0</td> <td>100</td> </tr> <tr> <td>VeriFuzz</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td>0</td> <td>100</td> <td>185</td> <td>90.81</td> </tr> </tbody> </table> <ul> <li>NoTermination property:</li> </ul> <table> <tbody> <tr> <td>SV-COMP Tool</td> <td>Function calls</td> <td>Threads</td> <td><strong>Assumptions</strong></td> <td><strong>Conditions</strong></td> <td>Thoroughness</td> <td>Error traces</td> <td>Validation rate</td> </tr> <tr> <td>2LS</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>50</td> <td>663</td> <td>69.08</td> </tr> <tr> <td>Bubaak</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>50</td> <td>578</td> <td>34.78</td> </tr> <tr> <td>CPAChecker</td> <td>1</td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>501</td> <td>97.01</td> </tr> <tr> <td>Symbiotic</td> <td>0</td> <td>1</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>50</td> <td>591</td> <td>52.96</td> </tr> <tr> <td>UAutomizer</td> <td>0.5</td> <td>1</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>100</td> <td>512</td> <td>98.24</td> </tr> <tr> <td>VeriFuzz</td> <td>0</td> <td>0</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>50</td> <td>492</td> <td>71.34</td> </tr> </tbody> </table> <ul> <li>ReachSafety property:</li> </ul> <table> <tbody> <tr> <td>SV-COMP Tool</td> <td><strong>Function calls</strong></td> <td>Threads</td> <td>Assumptions</td> <td>Conditions</td> <td>Thoroughness</td> <td>Error traces</td> <td>Validation rate</td> </tr> <tr> <td>Bubaak</td> <td><strong>0</strong></td> <td>0</td> <td>1</td> <td>0</td> <td>0</td> <td>24</td> <td>54.17</td> </tr> <tr> <td>CBMC</td> <td><strong>0</strong></td> <td>1</td> <td>1</td> <td>0</td> <td>0</td> <td>392</td> <td>1.28</td> </tr> <tr> <td>CPA-BAM-BnB</td> <td><strong>1</strong></td> <td>0</td> <td>1</td> <td>1</td> <td>100</td> <td>69</td> <td>85.51</td> </tr> <tr> <td>CPA-BAM-SMG</td> <td><strong>1</strong></td> <td>0</td> <td>1</td> <td>1</td> <td>100</td> <td>67</td> <td>85.07</td> </tr> <tr> <td>CPAChecker</td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>1</td> <td>100</td> <td>45</td> <td>88.89</td> </tr> <tr> <td>Crux</td> <td><strong>0</strong></td> <td>0</td> <td>1</td> <td>0</td> <td>0</td> <td>1572</td> <td>0.13</td> </tr> <tr> <td>ESBMC-kind</td> <td><strong>0</strong></td> <td>1</td> <td>1</td> <td>0</td> <td>0</td> <td>64</td> <td>21.88</td> </tr> <tr> <td>Graves-CPA</td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>1</td> <td>100</td> <td>66</td> <td>87.88</td> </tr> <tr> <td>Graves-Par</td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>1</td> <td>100</td> <td>24</td> <td>58.33</td> </tr> <tr> <td>PeSCo-CPA</td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>1</td> <td>100</td> <td>63</td> <td>85.71</td> </tr> </tbody> </table> <ul> <li>ConcurrencySafety property:</li> </ul> <table> <tbody> <tr> <td>SV-COMP Tool</td> <td><strong>Function calls</strong></td> <td><strong>Threads</strong></td> <td>Assumptions</td> <td>Conditions</td> <td>Thoroughness</td> <td>Error traces</td> <td>Validation rate</td> </tr> <tr> <td>CBMC</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>277</td> <td>87</td> </tr> <tr> <td>CPA-Lockator</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>83</td> <td>26.51</td> </tr> <tr> <td>CPAChecker</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>257</td> <td>100</td> </tr> <tr> <td>Cseq</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>100</td> <td>277</td> <td>94.58</td> </tr> <tr> <td>Dartagnan</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>0</td> <td>0</td> <td>50</td> <td>281</td> <td>92.17</td> </tr> <tr> <td>Deagle</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>280</td> <td>96.07</td> </tr> <tr> <td>DIVINE</td> <td><strong>0</strong></td> <td><strong>0</strong></td> <td>0</td> <td>0</td> <td>0</td> <td>230</td> <td>80.87</td> </tr> <tr> <td>EBF</td> <td><strong>0</strong></td> <td><strong>0</strong></td> <td>0</td> <td>0</td> <td>0</td> <td>282</td> <td>89.01</td> </tr> <tr> <td>ESBMC-incr</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>68</td> <td>79.41</td> </tr> <tr> <td>ESBMC-kind</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>263</td> <td>89.73</td> </tr> <tr> <td>Graves-CPA</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>261</td> <td>99.23</td> </tr> <tr> <td>Graves-Par</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>28</td> <td>100</td> </tr> <tr> <td>Infer</td> <td><strong>0</strong></td> <td><strong>0</strong></td> <td>0</td> <td>0</td> <td>0</td> <td>634</td> <td>0</td> </tr> <tr> <td>Lazy-CSeq</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>274</td> <td>94.89</td> </tr> <tr> <td>LF-checker</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>286</td> <td>85.31</td> </tr> <tr> <td>PeSCo-CPA</td> <td><strong>1</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>100</td> <td>256</td> <td>100</td> </tr> <tr> <td>PIChecker</td> <td><strong>1</strong></td> <td><strong>0</strong></td> <td>1</td> <td>1</td> <td>50</td> <td>269</td> <td>98.14</td> </tr> <tr> <td>Symbiotic</td> <td><strong>0</strong></td> <td><strong>1</strong></td> <td>1</td> <td>0</td> <td>50</td> <td>110</td> <td>92.73</td> </tr> <tr> <td>UAutomizer</td> <td><strong>0.5</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>75</td> <td>297</td> <td>94.95</td> </tr> <tr> <td>UgemCutter</td> <td><strong>0.5</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>75</td> <td>283</td> <td>96.47</td> </tr> <tr> <td>UTaipan</td> <td><strong>0.5</strong></td> <td><strong>1</strong></td> <td>1</td> <td>1</td> <td>75</td> <td>293</td> <td>96.25</td> </tr> </tbody> </table> <h3>5. Overall distance for all possible combinations of elements for thoroughness</h3> <p>This section presents the overall difference (i.e., the sum of differences between witness thoroughness and validation rates for each tool) when thoroughness is calculated based on all possible combinations of witness elements (assumptions, conditions, thread specifics, and function calls). The set of witnesses is the same as in the previous section. The following tables provide details for each property, with the minimum difference highlighted:</p> <ul> <li>MemSafety property:</li> </ul> <table> <tbody> <tr> <td>Combination</td> <td>Overall difference</td> </tr> <tr> <td>Function calls</td> <td>250.3</td> </tr> <tr> <td>Thread specifics</td> <td>444.6</td> </tr> <tr> <td>Assumptions</td> <td>353.7</td> </tr> <tr> <td>Conditions</td> <td>250.3</td> </tr> <tr> <td>Function calls, Thread specifics</td> <td>294.6</td> </tr> <tr> <td>Assumptions, Function calls</td> <td>238.08</td> </tr> <tr> <td>Conditions, Function calls</td> <td>250.3</td> </tr> <tr> <td>Assumptions, Thread specifics</td> <td>344.6</td> </tr> <tr> <td>Conditions, Thread specifics</td> <td>294.6</td> </tr> <tr> <td>Assumptions, Conditions</td> <td>238.08</td> </tr> <tr> <td>Assumptions, Function calls, Thread specifics</td> <td>277.94</td> </tr> <tr> <td>Conditions, Function calls, Thread specifics</td> <td>244.59</td> </tr> <tr> <td><strong>Assumptions, Conditions, Function calls</strong></td> <td><strong>221.41</strong></td> </tr> <tr> <td>Assumptions, Conditions, Thread specifics</td> <td>277.94</td> </tr> <tr> <td>Assumptions, Conditions, Function calls, Thread specifics</td> <td>244.6</td> </tr> </tbody> </table> <ul> <li>NoOverflow property:</li> </ul> <table> <tbody> <tr> <td>Combination</td> <td>Overall difference</td> </tr> <tr> <td>Function calls</td> <td>953.06</td> </tr> <tr> <td>Thread specifics</td> <td>745.4</td> </tr> <tr> <td><strong>Assumptions</strong></td> <td><strong>192.94</strong></td> </tr> <tr> <td>Conditions</td> <td>803.06</td> </tr> <tr> <td>Function calls, Thread specifics</td> <td>778.06</td> </tr> <tr> <td>Assumptions, Function calls</td> <td>478.06</td> </tr> <tr> <td>Conditions, Function calls</td> <td>878.06</td> </tr> <tr> <td>Assumptions, Thread specifics</td> <td>445.4</td> </tr> <tr> <td>Conditions, Thread specifics</td> <td>703.06</td> </tr> <tr> <td>Assumptions, Conditions</td> <td>403.06</td> </tr> <tr> <td>Assumptions, Function calls, Thread specifics</td> <td>528.8</td> </tr> <tr> <td>Conditions, Function calls, Thread specifics</td> <td>786.41</td> </tr> <tr> <td>Assumptions, Conditions, Function calls</td> <td>586.43</td> </tr> <tr> <td>Assumptions, Conditions, Thread specifics</td> <td>478.79</td> </tr> <tr> <td>Assumptions, Conditions, Function calls, Thread specifics</td> <td>590.56</td> </tr> </tbody> </table> <ul> <li>NoTermination property:</li> </ul> <table> <tbody> <tr> <td>Combination</td> <td>Overall difference</td> </tr> <tr> <td>Function calls</td> <td>279.39</td> </tr> <tr> <td>Thread specifics</td> <td>226.99</td> </tr> <tr> <td>Assumptions</td> <td>176.59</td> </tr> <tr> <td>Conditions</td> <td>232.91</td> </tr> <tr> <td>Function calls, Thread specifics</td> <td>204.39</td> </tr> <tr> <td><strong>Assumptions, Function calls</strong></td> <td><strong>84.83</strong></td> </tr> <tr> <td>Conditions, Function calls</td> <td>254.39</td> </tr> <tr> <td>Assumptions, Thread specifics</td> <td>107.43</td> </tr> <tr> <td>Conditions, Thread specifics</td> <td>182.91</td> </tr> <tr> <td>Assumptions, Conditions</td> <td>63.35</td> </tr> <tr> <td>Assumptions, Function calls, Thread specifics</td> <td>106.82</td> </tr> <tr> <td>Conditions, Function calls, Thread specifics</td> <td>212.73</td> </tr> <tr> <td>Assumptions, Conditions, Function calls</td> <td>112.74</td> </tr> <tr> <td>Assumptions, Conditions, Thread specifics</td> <td>93.67</td> </tr> <tr> <td>Assumptions, Conditions, Function calls, Thread specifics</td> <td>116.89</td> </tr> </tbody> </table> <ul> <li>ReachSafety property:</li> </ul> <table> <tbody> <tr> <td>Combination</td> <td>Overall difference</td> </tr> <tr> <td><strong>Function calls</strong></td> <td><strong>212.74</strong></td> </tr> <tr> <td>Thread specifics</td> <td>607.58</td> </tr> <tr> <td>Assumptions</td> <td>557.82</td> </tr> <tr> <td>Conditions</td> <td>312.74</td> </tr> <tr> <td>Function calls, Thread specifics</td> <td>357.58</td> </tr> <tr> <td>Assumptions, Function calls</td> <td>316.16</td> </tr> <tr> <td>Conditions, Function calls</td> <td>262.74</td> </tr> <tr> <td>Assumptions, Thread specifics</td> <td>507.32</td> </tr> <tr> <td>Conditions, Thread specifics</td> <td>407.58</td> </tr> <tr> <td>Assumptions, Conditions</td> <td>366.16</td> </tr> <tr> <td>Assumptions, Function calls, Thread specifics</td> <td>373.98</td> </tr> <tr> <td>Conditions, Function calls, Thread specifics</td> <td>307.56</td> </tr> <tr> <td>Assumptions, Conditions, Function calls</td> <td>299.48</td> </tr> <tr> <td>Assumptions, Conditions, Thread specifics</td> <td>407.32</td> </tr> <tr> <td>Assumptions, Conditions, Function calls, Thread specifics</td> <td>332.32</td> </tr> </tbody> </table> <ul> <li>ConcurrencySafety property:</li> </ul> <table> <tbody> <tr> <td>Combination</td> <td>Overall difference</td> </tr> <tr> <td>Function calls</td> <td>1016.62</td> </tr> <tr> <td>Thread specifics</td> <td>442.72</td> </tr> <tr> <td>Assumptions</td> <td>430.78</td> </tr> <tr> <td>Conditions</td> <td>980.44</td> </tr> <tr> <td>Function calls, Thread specifics</td> <td>637.9</td> </tr> <tr> <td>Assumptions, Function calls</td> <td>641.62</td> </tr> <tr> <td>Conditions, Function calls</td> <td>980.78</td> </tr> <tr> <td><strong>Assumptions, Thread specifics</strong></td> <td><strong>427.06</strong></td> </tr> <tr> <td>Conditions, Thread specifics</td> <td>626.72</td> </tr> <tr> <td>Assumptions, Conditions</td> <td>630.44</td> </tr> <tr> <td>Assumptions, Function calls, Thread specifics</td> <td>512.89</td> </tr> <tr> <td>Conditions, Function calls, Thread specifics</td> <td>735.42</td> </tr> <tr> <td>Assumptions, Conditions, Function calls</td> <td>739.14</td> </tr> <tr> <td>Assumptions, Conditions, Thread specifics</td> <td>510.03</td> </tr> <tr> <td>Assumptions, Conditions, Function calls, Thread specifics</td> <td>614.56</td> </tr> </tbody> </table> </div>