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] [Quick Jump]
- Data
- Documentation
- SBV
- Examples
- BitPrecise
- CodeGeneration
- Documentation.SBV.Examples.CodeGeneration.AddSub
- Documentation.SBV.Examples.CodeGeneration.CRC_USB5
- Documentation.SBV.Examples.CodeGeneration.Fibonacci
- Documentation.SBV.Examples.CodeGeneration.GCD
- Documentation.SBV.Examples.CodeGeneration.PopulationCount
- Documentation.SBV.Examples.CodeGeneration.Uninterpreted
- Crypto
- Existentials
- Lists
- Misc
- Documentation.SBV.Examples.Misc.Auxiliary
- Documentation.SBV.Examples.Misc.Enumerate
- Documentation.SBV.Examples.Misc.Floating
- Documentation.SBV.Examples.Misc.ModelExtract
- Documentation.SBV.Examples.Misc.NoDiv0
- Documentation.SBV.Examples.Misc.Polynomials
- Documentation.SBV.Examples.Misc.SoftConstrain
- Documentation.SBV.Examples.Misc.Word4
- Optimization
- Puzzles
- Documentation.SBV.Examples.Puzzles.Birthday
- Documentation.SBV.Examples.Puzzles.Coins
- Documentation.SBV.Examples.Puzzles.Counts
- Documentation.SBV.Examples.Puzzles.DogCatMouse
- Documentation.SBV.Examples.Puzzles.Euler185
- Documentation.SBV.Examples.Puzzles.Fish
- Documentation.SBV.Examples.Puzzles.Garden
- Documentation.SBV.Examples.Puzzles.HexPuzzle
- Documentation.SBV.Examples.Puzzles.LadyAndTigers
- Documentation.SBV.Examples.Puzzles.MagicSquare
- Documentation.SBV.Examples.Puzzles.NQueens
- Documentation.SBV.Examples.Puzzles.SendMoreMoney
- Documentation.SBV.Examples.Puzzles.Sudoku
- Documentation.SBV.Examples.Puzzles.U2Bridge
- Queries
- Documentation.SBV.Examples.Queries.AllSat
- Documentation.SBV.Examples.Queries.CaseSplit
- Documentation.SBV.Examples.Queries.Enums
- Documentation.SBV.Examples.Queries.FourFours
- Documentation.SBV.Examples.Queries.GuessNumber
- Documentation.SBV.Examples.Queries.Interpolants
- Documentation.SBV.Examples.Queries.UnsatCore
- Strings
- Uninterpreted
- Examples
- SBV
Downloads
- sbv-7.13.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)