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/ _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
