CBMC - Bounded Model Checking for ANSI-C
CBMC
Homepage
example invocation of
cbmc
cbmc t.c --function insert --unwind 8 --decide