Keywords: Software verification · Program analysis · Software validation · Software bugs · Verification witnesses · Evaluation · Benchmarking
Category | Witnesses | CPAchecker | CPA-w2t | CProver-w2t | Dartgnan | MetaVal | nitwit | Symbiotic -Witch | UAutomizer |
ReachSafety | |||||||||
valid∗ | 26797 | 14908 | 8628 | 14168 | – | 0 | 15507 | 11176 | 8592 |
invalid | 5 177 | 28 | 12 | 2 | – | 0 | 10 | 0 | 0 |
MemSafety | |||||||||
valid∗ | 16984 | 12594 | 231 | 954 | – | 116 | – | 8394 | 4197 |
invalid | 2 804 | 0 | 0 | 26 | – | 2 | – | 0 | 0 |
ConcurrencySafety | |||||||||
valid∗ | 4746 | 2700 | – | – | 1464 | – | – | – | – |
invalid | 1293 | 40 | – | – | 0 | – | – | – | – |
NoOverflows | |||||||||
valid∗ | 2808 | 2334 | 887 | 1436 | – | 1982 | – | 2609 | 2468 |
invalid | 167 | 0 | 0 | 0 | – | 0 | – | 0 | 0 |
Termination | |||||||||
valid∗ | 3652 | 2580 | – | – | – | 598 | – | – | 960 |
invalid | 56 | 21 | – | – | – | 0 | – | – | 0 |
SoftwareSystems | |||||||||
valid∗ | 2102 | 621 | 6 | 33 | – | 0 | 0 | 179 | 26 |
invalid | 5903 | 5 | 0 | 27 | – | 0 | 0 | 51 | 4 |
Category | Witnesses | CPAchecker | MetaVal | UAutomizer |
ReachSafety | ||||
valid∗ | 31013 | 17312 | 19655 | 19632 |
invalid | 894 | 0 | 315 | 3 |
MemSafety | ||||
valid∗ | 16948 | – | 227 | 14384 |
invalid | 326 | – | 0 | 0 |
ConcurrencySafety | ||||
valid∗ | 3177 | – | – | – |
invalid | 389 | – | – | – |
NoOverflows | ||||
valid∗ | 2089 | 1718 | 1608 | 1713 |
invalid | 300 | 0 | 36 | 0 |
Termination | ||||
valid∗ | 4502 | – | – | – |
invalid | 14 | – | – | – |
SoftwareSystems | ||||
valid∗ | 25819 | 6771 | 20624 | 19343 |
invalid | 888 | 0 | 403 | 0 |