The afv package
AFV is an infinite state model checker that verifies iterative C programs by k-induction. AFV uses Yices as the backend SMT solver.
Properties
| Versions | 0.0.0, 0.0.1, 0.0.2, 0.0.3, 0.0.4, 0.1.0, 0.1.1 |
|---|---|
| Dependencies | base (4.*), bytestring (≥0.9 & <1.0), directory (1.0.*), language-c (≥0.3.1.1), mtl (1.1.*), process (1.0.*), yices (≥0.0.0.6) |
| License | BSD3 |
| Author | Tom Hawkins <tomahawkins@gmail.com> |
| Maintainer | Tom Hawkins <tomahawkins@gmail.com> |
| Stability | experimental |
| Category | Formal Methods |
| Home page | http://tomahawkins.org |
| Source repository | darcs get http://patch-tag.com/r/tomahawkins/afv/pullrepo |
| Executables | afv |
| Upload date | Mon Jan 25 04:24:12 UTC 2010 |
| Uploaded by | TomHawkins |
Downloads
- afv-0.1.0.tar.gz (Cabal source package)
- package description (included in the package)