Overview of verifiers from SV-COMP 2020

We are searching for verifiers that:

  1. Can correctly solve tasks that CPAchecker cannot solve (1.1) and vice versa (1.2)
  2. Have a “high quality” in their correctness witnesses. This means, that the invariants generated are
    1. valid C expressions without intermediate variables introduced by the verifiers pre-processing, and
    2. are in fact helpfull proving the program correct (not trivial, like ‘true’ or i <= MAXINT for int i)
Tool (1.1) (1.2) (2.1) (2.2)
2ls 71 2474 Yes No
brick 39 3699 Yes No
cbmc 150 2659 No Yes
cpa-seq 0 0 Yes Yes
divine 67 3161 Yes No
esbmc 327 796 Yes No
gacal 30 4040 Yes^2 Yes
map2check 259 3673 Yes No
Pinaka 174 1550 No No
PredatorHP 28 2 No No
Symbiotic 204 1159 No No
UAutomizer 216 894 Yes^1 Yes
UKojak 38 1938 Yes^1 Yes
UTaipan 69 1291 Yes^1 Yes
VeriAbs 897 87 Yes Sometimes
VeriFuzz 214 1661 No No

1: The Ultimate Framework produces witnesses that CPAchecker can not parse (several witness-automaton transitions for a single statement). This issue can be (and is) circumvented with a post-processing step that merges all witness-automaton transitions for a single statement into one transition.

2: CPAchecker can not parse any of the witnesses of GACAL.

Comments to each verifier: