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 | git clone git://github.com/tomahawkins/afv.git |
| Executables | afv |
| Upload date | Wed Mar 31 03:08:55 UTC 2010 |
| Uploaded by | TomHawkins |
Downloads
- afv-0.1.1.tar.gz (Cabal source package)
- package description (included in the package)