Interpretation-Based Violation Witness Validation for C: NITWIT
49
Fig. 2: Validator outcomes on 11 533 witnesses from SV-COMP 2020.
Producing output false. With the result False, validators indicate they have
found a property violation, i.e., a reachable error location. These results are of
particular interest, as the dataset used for our evaluation contains witnesses only
for programs deemed incorrect.
For 10 933 witnesses at least one validator validated the verification result.
Figure 3 presents a Venn diagram that displays the partitioning of these witnesses
between validators based on shared successful validations. The shape as a whole
stands for all of the validated witnesses and each validator is represented by
a distinctly colored enclosure. Circles group intersecting results and the bigger
numbers inside describe their cardinality. The smaller numbers underneath are
for making clear which validators belong to the group (ordering is from top
to bottom, so CPAchecker is number one and so on). The diagram reveals
that only about 226 witnesses are approved by all verifiers, though the largest
shared subset has 2 010 of them – it corresponds to results shared by all of the
validators with exception of Ultimate Automizer and MetaVal. In total,
1 411 instances are validated only once, 1 878 twice, 2 290 thrice, 3 682 four times
and 1 446 five times. nitwit validates 399 witnesses that no other tool validates.
Interestingly, none of the validators subsume each other in terms of False results,
each has some not negligible amount of witnesses validated uniquely.
Concerning resource usage, Figure 4(a) depicts the reached number of successfully validated witnesses plotted against the required CPU time (in logscale). Data points are sorted by the required CPU time and the black line at
the top marks the timeout. nitwit finds violations systematically faster than
any other tool. Its mean runtime amounts to 0.63 seconds, the median was noticeably smaller at 0.02 seconds, standard deviation was 4.74. The runtime for
nitwit is skewed towards zero with most results achieved under half a second.
We also see that running nitwit more than 10 seconds scarcely produces any
new results. That is not the case for CPAchecker, Ultimate Automizer,
MetaVal and CPA-witness2test, which frequently need more than that,
49
Fig. 2: Validator outcomes on 11 533 witnesses from SV-COMP 2020.
Producing output false. With the result False, validators indicate they have
found a property violation, i.e., a reachable error location. These results are of
particular interest, as the dataset used for our evaluation contains witnesses only
for programs deemed incorrect.
For 10 933 witnesses at least one validator validated the verification result.
Figure 3 presents a Venn diagram that displays the partitioning of these witnesses
between validators based on shared successful validations. The shape as a whole
stands for all of the validated witnesses and each validator is represented by
a distinctly colored enclosure. Circles group intersecting results and the bigger
numbers inside describe their cardinality. The smaller numbers underneath are
for making clear which validators belong to the group (ordering is from top
to bottom, so CPAchecker is number one and so on). The diagram reveals
that only about 226 witnesses are approved by all verifiers, though the largest
shared subset has 2 010 of them – it corresponds to results shared by all of the
validators with exception of Ultimate Automizer and MetaVal. In total,
1 411 instances are validated only once, 1 878 twice, 2 290 thrice, 3 682 four times
and 1 446 five times. nitwit validates 399 witnesses that no other tool validates.
Interestingly, none of the validators subsume each other in terms of False results,
each has some not negligible amount of witnesses validated uniquely.
Concerning resource usage, Figure 4(a) depicts the reached number of successfully validated witnesses plotted against the required CPU time (in logscale). Data points are sorted by the required CPU time and the black line at
the top marks the timeout. nitwit finds violations systematically faster than
any other tool. Its mean runtime amounts to 0.63 seconds, the median was noticeably smaller at 0.02 seconds, standard deviation was 4.74. The runtime for
nitwit is skewed towards zero with most results achieved under half a second.
We also see that running nitwit more than 10 seconds scarcely produces any
new results. That is not the case for CPAchecker, Ultimate Automizer,
MetaVal and CPA-witness2test, which frequently need more than that,