AFV is an infinite state model checker for simple, iterative C programs. This release adds some new name checks, a few minor bug fixes, basic support for functions, and a little stronger type checking. Though most of the C language is still not supported, it can verify a lot of interesting behavior -- including one of my bugs that pulverized about $40K of hydraulics hardware last year. :-) http://hackage.haskell.org/package/afv/