Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Tom Hawkins <tomahawkins <at> gmail.com>
Subject: ANN: afv-0.1.0
Newsgroups: gmane.comp.lang.haskell.cafe
Date: Monday 25th January 2010 04:47:10 UTC (over 6 years ago)
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
 
CD: 3ms