48
J. ˇ
Svejda et al.
output automata that lead directly to the error location. Not many specify information about function enter and return. Except for VeriFuzz, Map2Check
and Symbiotic, tools usually put assumptions on edges selectively, though there
are also some that do not use them – DIVINE and PredatorHP. Assumptions are an important part of witness automata, they restrict the exploration of
state space and potentially save the most work during validation. Nevertheless,
having to check a large number of them may prove difficult. On the whole, an
average witness has around 2 000 nodes, 2 200 transitions between them, 1 300
state-space guards in form of assumptions, 360 controls for branching conditions, 15 function calls and return guards. The largest witness was produced
by Pinaka and contains 2.1 million nodes and transitions with assumptions on
almost half of them.
5.2 Evaluation Setting
The runtime was limited to 90 s, while memory was limited to 7 GB [6]. Based
on recorded data and extracted results, we distinguish six different outcomes of
a validator:
False Validator found that an error location is reachable in the program. This
is the desired result, nevertheless, be aware that not all witnesses in the
available dataset necessarily describe valid violation paths.
Unknown The validator could not find a definite answer.
True The validator claims the program does not reach an error location in the
state-space restricted by the witness.
Timeout The validator exceeded the granted CPU time before reaching an
answer.
Error An error occurred in the validator during computation (not in the program under inspection). Includes errors due to malformed witnesses.
Out of memory The validator exceeded the allowed amount of memory.
5.3 Experimental Results
Figure 2 presents the results on validating 11 533 witnesses by the five violation witness validators. Note that sometimes validator names in tables or plots
are abbreviated for readability. The colors discern the possible outcomes described above. The validators are sorted in ascending order by the number of
False results (blue). nitwit and CPAchecker manage to find the most violations (8 526 and 7 642 respectively), closely followed by FShell-witness2test
(7 005). CPA-witness2test is able to validate 6 104, Ultimate Automizer
finds 4 393 and MetaVal 1 681.
All validators except for nitwit output True (green) in some cases, which
means the validator rejected the witness. Ultimate Automizer rejects the
majority of witnesses during validation. CPA-witness2test shows the highest
ratio of Unknown results, whereas FShell-witness2test exhibits the largest
amount of unaccepted witnesses due to malformation (Bad witness). MetaVal
exceeds the alloted time in most cases. The results are detailed in Table 2 on
page 52.
J. ˇ
Svejda et al.
output automata that lead directly to the error location. Not many specify information about function enter and return. Except for VeriFuzz, Map2Check
and Symbiotic, tools usually put assumptions on edges selectively, though there
are also some that do not use them – DIVINE and PredatorHP. Assumptions are an important part of witness automata, they restrict the exploration of
state space and potentially save the most work during validation. Nevertheless,
having to check a large number of them may prove difficult. On the whole, an
average witness has around 2 000 nodes, 2 200 transitions between them, 1 300
state-space guards in form of assumptions, 360 controls for branching conditions, 15 function calls and return guards. The largest witness was produced
by Pinaka and contains 2.1 million nodes and transitions with assumptions on
almost half of them.
5.2 Evaluation Setting
The runtime was limited to 90 s, while memory was limited to 7 GB [6]. Based
on recorded data and extracted results, we distinguish six different outcomes of
a validator:
False Validator found that an error location is reachable in the program. This
is the desired result, nevertheless, be aware that not all witnesses in the
available dataset necessarily describe valid violation paths.
Unknown The validator could not find a definite answer.
True The validator claims the program does not reach an error location in the
state-space restricted by the witness.
Timeout The validator exceeded the granted CPU time before reaching an
answer.
Error An error occurred in the validator during computation (not in the program under inspection). Includes errors due to malformed witnesses.
Out of memory The validator exceeded the allowed amount of memory.
5.3 Experimental Results
Figure 2 presents the results on validating 11 533 witnesses by the five violation witness validators. Note that sometimes validator names in tables or plots
are abbreviated for readability. The colors discern the possible outcomes described above. The validators are sorted in ascending order by the number of
False results (blue). nitwit and CPAchecker manage to find the most violations (8 526 and 7 642 respectively), closely followed by FShell-witness2test
(7 005). CPA-witness2test is able to validate 6 104, Ultimate Automizer
finds 4 393 and MetaVal 1 681.
All validators except for nitwit output True (green) in some cases, which
means the validator rejected the witness. Ultimate Automizer rejects the
majority of witnesses during validation. CPA-witness2test shows the highest
ratio of Unknown results, whereas FShell-witness2test exhibits the largest
amount of unaccepted witnesses due to malformation (Bad witness). MetaVal
exceeds the alloted time in most cases. The results are detailed in Table 2 on
page 52.