Interpretation-Based Violation Witness Validation for C: NITWIT
51
204
(1)
313
(1, 2)
23
(1, 2, 3)
156
(1, 2, 3, 4)
6
(1, 2, 3, 4, 5)
226
(1, 2, 3, 4, 5, 6)
539
(2)
10
(2, 3)
15
(2, 3, 4)
64
(2, 3, 4, 5, 6)
40
(2, 4)
11
(2, 4, 5)
33
(2, 4, 5, 6)
52
(2, 4, 6)
18
(2, 5)
1
(2, 3, 5)
3
(2, 3, 5, 6)
7
(2, 5, 6)
121
(2, 6)
97
(2, 3, 6)
108
(2, 3, 4, 6)
44
(3)
6
(1, 3)
28
(1, 3, 4)
10
(1, 3, 4, 5)
343
(1, 3, 4, 5, 6)
237
(3, 4)
4
(3, 4, 5)
68
(3, 4, 5, 6)
405
(3, 4, 6)
2
(3, 5)
7
(1, 3, 5)
31
(3, 6)
488
(1, 3, 6)
2010
(1, 3, 4, 6)
179
(4)
67
(1, 4)
123
(1, 2, 4)
47
(1, 2, 4, 5)
31
(1, 2, 4, 5, 6)
15
(4, 5)
100
(1, 4, 5)
115
(1, 4, 5, 6)
39
(4, 5, 6)
650
(4, 6)
662
(1, 4, 6)
213
(1, 2, 4, 6)
46
(5)
59
(1, 5)
96
(1, 2, 5)
1
(1, 2, 3, 5)
54
(1, 2, 3, 5, 6)
53
(5, 6)
13
(1, 5, 6)
209
(1, 2, 5, 6)
399
(6)
256
(1, 6)
119
(1, 2, 6)
709
(1, 2, 3, 6)
948
(1, 2, 3, 4, 6)
CPAchecker
Ult. Auto.
CPA-w2t
FShell-w2t
MetaVal
NITWIT
Fig. 3: A Venn diagram showing the coverage of False validation results by
various validators.
(a) CPU time (seconds) in validations
for result False.
(b) Memory consumption (in MB) during validations for result False.
(c) CPU time (seconds) in validations
for all results.
(d) Memory consumption (in MB) in
validations for all results.
Fig. 4: Resources for results False (first row) and all together (second row).