[Haskell-cafe] ANN: afv-0.1.0
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...
- type casts
- static top-level declarations
- non void functions
- switch statements
- arbitrary loop statements
More information about the Haskell-Cafe