7July_22_2008 ANSI-C bounded model checker user manual...
overview----
CBMC
translates .c program and merges function defs of *.c files, like a linker and gives symbolic simulation
prints verification conditions it generates as a Gentzen sequent (comment w/ sequent)
CNF then to SAT-solver
CBMC does not guess preconditions
unwinds for loops
-array bounds
-checks unwinding
-proves runt times bounds
=> gives counter-example
...