afv-0.0.4: afv.cabal
name: afv
version: 0.0.4
category: Formal Methods
synopsis: Infinite state model checking of iterative C programs.
description: AFV is an infinite state model checker that
verifies iterative C programs by k-induction.
AFV uses Yices as the backend SMT solver.
author: Tom Hawkins <tomahawkins@gmail.com>
maintainer: Tom Hawkins <tomahawkins@gmail.com>
stability: experimental
license: BSD3
license-file: LICENSE
homepage: http://tomahawkins.org
build-type: Simple
cabal-version: >= 1.6
extra-source-files:
RELEASE-NOTES
executable afv
hs-source-dirs: src
main-is: AFV.hs
other-modules: Compile,
Error,
Model,
Parse,
Utils,
Verify
build-depends:
base >= 4 && < 5,
bytestring >= 0.9 && < 1.0,
mtl >= 1.1 && < 1.2,
directory >= 1.0 && < 1.1,
process >= 1.0 && < 1.1,
language-c >= 0.3.1.1,
yices >= 0.0.0.6
ghc-options: -W
extensions:
source-repository head
type: darcs
location: http://patch-tag.com/r/tomahawkins/afv/pullrepo