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 ]
This version is deprecated.
Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers.
[Skip to Readme]
Modules
[Index] [Quick Jump]
- Data
- Data.SBV
- Data.SBV.Char
- Data.SBV.Control
- Data.SBV.Dynamic
- Data.SBV.Either
- Data.SBV.Float
- Data.SBV.Internals
- Data.SBV.List
- Data.SBV.Maybe
- Data.SBV.Rational
- Data.SBV.RegExp
- Data.SBV.Set
- Data.SBV.String
- Tools
- Data.SBV.Tools.BMC
- Data.SBV.Tools.BVOptimize
- Data.SBV.Tools.BoundedFix
- Data.SBV.Tools.BoundedList
- Data.SBV.Tools.CodeGen
- Data.SBV.Tools.GenTest
- Data.SBV.Tools.Induction
- Data.SBV.Tools.NaturalInduction
- Data.SBV.Tools.Overflow
- Data.SBV.Tools.Polynomial
- Data.SBV.Tools.Range
- Data.SBV.Tools.STree
- Data.SBV.Tools.WeakestPreconditions
- Data.SBV.Trans
- Data.SBV.Tuple
- Data.SBV
- 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
- DeltaSat
- Existentials
- Lists
- Misc
- Documentation.SBV.Examples.Misc.Auxiliary
- Documentation.SBV.Examples.Misc.Definitions
- Documentation.SBV.Examples.Misc.Enumerate
- Documentation.SBV.Examples.Misc.FirstOrderLogic
- Documentation.SBV.Examples.Misc.Floating
- Documentation.SBV.Examples.Misc.LambdaArray
- Documentation.SBV.Examples.Misc.ModelExtract
- Documentation.SBV.Examples.Misc.NestedArray
- Documentation.SBV.Examples.Misc.Newtypes
- Documentation.SBV.Examples.Misc.NoDiv0
- Documentation.SBV.Examples.Misc.Polynomials
- Documentation.SBV.Examples.Misc.ProgramPaths
- Documentation.SBV.Examples.Misc.SetAlgebra
- Documentation.SBV.Examples.Misc.SoftConstrain
- Documentation.SBV.Examples.Misc.Tuple
- Optimization
- ProofTools
- Puzzles
- Documentation.SBV.Examples.Puzzles.AOC_2021_24
- Documentation.SBV.Examples.Puzzles.Birthday
- Documentation.SBV.Examples.Puzzles.Coins
- Documentation.SBV.Examples.Puzzles.Counts
- Documentation.SBV.Examples.Puzzles.DogCatMouse
- Documentation.SBV.Examples.Puzzles.Drinker
- Documentation.SBV.Examples.Puzzles.Euler185
- Documentation.SBV.Examples.Puzzles.Fish
- Documentation.SBV.Examples.Puzzles.Garden
- Documentation.SBV.Examples.Puzzles.HexPuzzle
- Documentation.SBV.Examples.Puzzles.Jugs
- Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
- Documentation.SBV.Examples.Puzzles.LadyAndTigers
- Documentation.SBV.Examples.Puzzles.MagicSquare
- Documentation.SBV.Examples.Puzzles.Murder
- Documentation.SBV.Examples.Puzzles.NQueens
- Documentation.SBV.Examples.Puzzles.Newspaper
- Documentation.SBV.Examples.Puzzles.Orangutans
- Documentation.SBV.Examples.Puzzles.Rabbits
- Documentation.SBV.Examples.Puzzles.SendMoreMoney
- Documentation.SBV.Examples.Puzzles.Sudoku
- Documentation.SBV.Examples.Puzzles.Tower
- Documentation.SBV.Examples.Puzzles.U2Bridge
- Queries
- Documentation.SBV.Examples.Queries.Abducts
- Documentation.SBV.Examples.Queries.AllSat
- Documentation.SBV.Examples.Queries.CaseSplit
- Documentation.SBV.Examples.Queries.Concurrency
- 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
- Transformers
- Uninterpreted
- Documentation.SBV.Examples.Uninterpreted.AUF
- Documentation.SBV.Examples.Uninterpreted.Deduce
- Documentation.SBV.Examples.Uninterpreted.Function
- Documentation.SBV.Examples.Uninterpreted.Multiply
- Documentation.SBV.Examples.Uninterpreted.Shannon
- Documentation.SBV.Examples.Uninterpreted.Sort
- Documentation.SBV.Examples.Uninterpreted.UISortAllSat
- WeakestPreconditions
- Documentation.SBV.Examples.WeakestPreconditions.Append
- Documentation.SBV.Examples.WeakestPreconditions.Basics
- Documentation.SBV.Examples.WeakestPreconditions.Fib
- Documentation.SBV.Examples.WeakestPreconditions.GCD
- Documentation.SBV.Examples.WeakestPreconditions.IntDiv
- Documentation.SBV.Examples.WeakestPreconditions.IntSqrt
- Documentation.SBV.Examples.WeakestPreconditions.Length
- Documentation.SBV.Examples.WeakestPreconditions.Sum
- Examples
- SBV
Downloads
- sbv-10.11.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates