[nanolith]

For C model checking, I use CBMC. It is a great tool, but it does take some finesse to use well.

http://www.cprover.org/cbmc/