24 Jan
2010
24 Jan
'10
11:47 p.m.
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