SPIN: I haven't tried it. I read the manual and find out that SPIN use its own language Promela, so I have to change the C code. And the manual also says that "Spin is a tool for analyzing the logical consistency of concurrent systems, specifically of data communication protocols". So I think it's not suitable. (http://spinroot.com/spin/sitemap.html)

MAGIC: I haven't tried it either. However after I read the introduction and tutorial, I think it might be a very good tools for us. It's used to verify an implementation in C code conforms to its specification. (http://www.cs.cmu.edu/~chaki/magic/)

CBMC: I've tried this tool. It's a Bounded Model Checker for ANSI-C programs. It allows verifying array bounds, pointer safety and user-specified assertions. It's kind of useful, but not performs well with loops in C code. (http://www-2.cs.cmu.edu/~modelcheck/cbmc/)

VeriSoft: I an unable to download the software. It seems to be useful, but I am not sure if it can deal with multiplication. (http://cm.bell-labs.com/who/god/verisoft/files.html)

BANDERA: for model checking concurrent Java software. not for me. (http://bandera.projects.cis.ksu.edu/)

FSP notation: might be useful (http://www.doc.ic.ac.uk/~jnm/LTSdocumention/FSP-notation.html)