sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
[ bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ]
[ Propose Tags ]
Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers.
For details, please see: http://leventerkok.github.com/sbv/
Release notes: http://github.com/LeventErkok/sbv/blob/master/CHANGES.md
[Skip to Readme]
Modules
[Index]
- Data
- Data.SBV
- Bridge
- Examples
- BitPrecise
- CodeGeneration
- Crypto
- Existentials
- Misc
- Polynomials
- Puzzles
- Uninterpreted
- Data.SBV.Internals
- Data.SBV
Downloads
- sbv-4.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)