[Haskell-cafe] ANN: afv-0.1.0

Tom Hawkins tomahawkins at gmail.com
Sun Jan 24 23:47:10 EST 2010

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


More information about the Haskell-Cafe mailing list