bounded model checker for C and C++ programs

 CBMC generates traces that demonstrate how an assertion can be violated, or
 proves that the assertion cannot be violated within a given number of loop
 iterations.