[Haskell-cafe] ANN: afv-0.1.0

[Tom Hawkins]

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