52
J. ˇ
Svejda et al.
12.0 seconds, 16.0 seconds, 96.0 seconds for Nitwit, FShell-witness2test,
CPA-witness2test, CPAchecker, Ultimate Automizer and MetaVal
respectively.
Figure 5 shows how nitwit compares to the other four validators in terms
of time and successful validation results. In each plot, a validator is compared
against nitwit. Witnesses validated by both have a blue color, validated only
by nitwit yellow, by the other tool green and any other are depicted in red. The
diagonal line is supplemented by two other lines representing a ±30% difference
in CPU time. The result, if not false, is plotted on one of six lines at the end
of its axis. These lines correspond to a Timeout (abbreviated by to), Unknown
(uk ), True (tu), Error (er ) and Out of memory (om). Every point represents a
witness (identical for both validators).
Figure 5 shows that in instances of agreed False results, nitwit is always
faster than other validators. FShell-witness2test has 1 114 validations within
less than one second difference. This is 0 for all of the others.
Verifier
CPAchecker Ult. Auto. CPA-w2t FS-w2t MetaVal NITWIT Virt. best Total
2LS
114
164
166
358
91
332
477
563
BRICK
20
11
38
36
17
38
42
43
CBMC
171
423
456
358
114
488
768
905
CPAchecker
1091
713
927
491
0
1070
1171
1189
DIVINE
400
46
110
280
181
237
448
460
ESBMC
572
131
605
843
249
730
955
1022
GACAL
0
10
0
10
7
15
15
15
Map2Check
80
32
106
129
120
137
211
264
PeSCo
1030
625
845
606
0
988
1064
1081
Pinaka
531
518
541
454
54
440
616
629
PredatorHP
55
35
18
44
53
20
69
70
Symbiotic
1033
12
866
894
134
1047
1103
1106
UAutomizer
391
574
55
189
159
233
630
662
UKojak
291
310
38
151
135
179
348
348
UTaipan
370
379
53
189
150
205
427
452
VeriAbs
501
366
326
892
10
1139
1298
1427
VeriFuzz
992
44
954
1081
207
1228
1291
1297
Total
7642
4393
6104
7005
1681
8526
10933 11533
Table 2: Results on successful validations of violation witnesses generated by the
various verifiers. Column Virtual best aggregates witnesses that are validated at
least once.
5.4 Discussion
Nondeterminism in programs. nitwit is not designed for proving a program
correct with respect to some specification, because the validator explores only a
single path. Nevertheless, to prove a program incorrect it may suffice to look at
a single path and although the program may contain nondeterministic choices
(e.g., if a condition depends on a nondeterministic variable) – if these are resolved
using a witness, then the execution becomes deterministic. This is the main idea
behind execution- and interpretation-based validators, because after resolving
J. ˇ
Svejda et al.
12.0 seconds, 16.0 seconds, 96.0 seconds for Nitwit, FShell-witness2test,
CPA-witness2test, CPAchecker, Ultimate Automizer and MetaVal
respectively.
Figure 5 shows how nitwit compares to the other four validators in terms
of time and successful validation results. In each plot, a validator is compared
against nitwit. Witnesses validated by both have a blue color, validated only
by nitwit yellow, by the other tool green and any other are depicted in red. The
diagonal line is supplemented by two other lines representing a ±30% difference
in CPU time. The result, if not false, is plotted on one of six lines at the end
of its axis. These lines correspond to a Timeout (abbreviated by to), Unknown
(uk ), True (tu), Error (er ) and Out of memory (om). Every point represents a
witness (identical for both validators).
Figure 5 shows that in instances of agreed False results, nitwit is always
faster than other validators. FShell-witness2test has 1 114 validations within
less than one second difference. This is 0 for all of the others.
Verifier
CPAchecker Ult. Auto. CPA-w2t FS-w2t MetaVal NITWIT Virt. best Total
2LS
114
164
166
358
91
332
477
563
BRICK
20
11
38
36
17
38
42
43
CBMC
171
423
456
358
114
488
768
905
CPAchecker
1091
713
927
491
0
1070
1171
1189
DIVINE
400
46
110
280
181
237
448
460
ESBMC
572
131
605
843
249
730
955
1022
GACAL
0
10
0
10
7
15
15
15
Map2Check
80
32
106
129
120
137
211
264
PeSCo
1030
625
845
606
0
988
1064
1081
Pinaka
531
518
541
454
54
440
616
629
PredatorHP
55
35
18
44
53
20
69
70
Symbiotic
1033
12
866
894
134
1047
1103
1106
UAutomizer
391
574
55
189
159
233
630
662
UKojak
291
310
38
151
135
179
348
348
UTaipan
370
379
53
189
150
205
427
452
VeriAbs
501
366
326
892
10
1139
1298
1427
VeriFuzz
992
44
954
1081
207
1228
1291
1297
Total
7642
4393
6104
7005
1681
8526
10933 11533
Table 2: Results on successful validations of violation witnesses generated by the
various verifiers. Column Virtual best aggregates witnesses that are validated at
least once.
5.4 Discussion
Nondeterminism in programs. nitwit is not designed for proving a program
correct with respect to some specification, because the validator explores only a
single path. Nevertheless, to prove a program incorrect it may suffice to look at
a single path and although the program may contain nondeterministic choices
(e.g., if a condition depends on a nondeterministic variable) – if these are resolved
using a witness, then the execution becomes deterministic. This is the main idea
behind execution- and interpretation-based validators, because after resolving