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/
[Skip to Readme]
Modules
[Index]
- Data
- Data.SBV
- Bridge
- Data.SBV.Dynamic
- Examples
- BitPrecise
- CodeGeneration
- Crypto
- Existentials
- Misc
- Polynomials
- Puzzles
- Data.SBV.Examples.Puzzles.Birthday
- Data.SBV.Examples.Puzzles.Coins
- Data.SBV.Examples.Puzzles.Counts
- Data.SBV.Examples.Puzzles.DogCatMouse
- Data.SBV.Examples.Puzzles.Euler185
- Data.SBV.Examples.Puzzles.Fish
- Data.SBV.Examples.Puzzles.MagicSquare
- Data.SBV.Examples.Puzzles.NQueens
- Data.SBV.Examples.Puzzles.SendMoreMoney
- Data.SBV.Examples.Puzzles.Sudoku
- Data.SBV.Examples.Puzzles.U2Bridge
- Uninterpreted
- Data.SBV.Internals
- Data.SBV
Downloads
- sbv-5.12.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)