CBMC ist pretty cool, I've used it in my bachelor's thesis for verification of fairness properties in proportional voting. Another use case I've seen is using C

CBMC ist pretty cool, I've used it in my bachelor's thesis for verification of fairness properties in proportional voting. Another use case I've seen is using CBMC in multiparty computation. What you have there is methods that work on boolean circuits. Flange CBMC in front of this and you got multiparty computation of C code.