packages feed

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