AFV is an infinite state model checker to verify assertions in embedded C programs.
New in this release: - Starts analysis from 'main' entry point. Automatically identifies the main loop (for (;;), while (1)). - Better counter example generation. - Enforces stateless expressions. Unfortunately, the list of unsupported C is still long. No... - arrays - pointers - structs - unions - typedefs - type casts - static top-level declarations - non void functions - switch statements - arbitrary loop statements http://hackage.haskell.org/package/afv _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
