Name: sbv
Version: 2.8
x-revision: 1
Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Description: Express properties about Haskell programs and automatically prove them using SMT
(Satisfiability Modulo Theories) solvers. Automatically generate C programs from
Haskell functions. The SBV library adds support for symbolic bit vectors and other
symbolic types, allowing formal models of Haskell programs to be created.
.
> $ ghci -XScopedTypeVariables
> Prelude> :m Data.SBV
> Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
> Q.E.D.
> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
> Falsifiable. Counter-example:
> x = 128 :: SWord8
.
The SBV library uses Microsoft's Z3 SMT solver () as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (), although the Z3 binding is much more richer.
.
SBV introduces the following types and concepts:
.
* 'SBool': Symbolic Booleans (bits)
.
* 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)
.
* 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed)
.
* 'SInteger': Symbolic unbounded integers (signed)
.
* 'SReal': Symbolic algebraic reals (signed)
.
* 'SArray', 'SFunArray': Flat arrays of symbolic values
.
* 'STree': Full binary trees of symbolic values (for fast symbolic access)
.
* Symbolic polynomials over GF(2^n), and polynomial arithmetic
.
* Uninterpreted constants and functions over symbolic values, with user defined axioms.
.
* Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
.
Functions built out of these types can be:
.
* proven correct via an external SMT solver (the 'prove' function)
.
* checked for satisfiability (the 'sat', and 'allSat' functions)
.
* used in synthesis (the 'sat' function with existential variables)
.
* optimized with respect to cost functions (the 'optimize', 'maximize',
and 'minimize' functions)
.
* quick-checked
.
* used in concrete test case generation (the 'genTest' function), rendered as
values in various languages, including Haskell and C.
.
Predicates can have both existential and universal variables. Use of
alternating quantifiers provides considerable expressive power.
Furthermore, existential variables allow synthesis via model generation.
.
The SBV library can also compile Haskell functions that manipulate symbolic
values directly to C, rendering them as straight-line C programs.
.
In addition to the library, the installation will create the
executable @SBVUnitTests@. You should run it once the installation is complete,
to make sure the unit tests are run and all is well.
.
SBV is hosted at GitHub: . Comments,
bug reports, and patches are always welcome.
.
The following people reported bugs, provided comments/feedback, or contributed to the
development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John
Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and
Nis Wegmann.
.
Release notes can be seen at: .
Copyright: Levent Erkok, 2010-2012
License: BSD3
License-file: LICENSE
Stability: Experimental
Author: Levent Erkok
Homepage: http://github.com/LeventErkok/sbv
Bug-reports: http://github.com/LeventErkok/sbv/issues
Maintainer: Levent Erkok (erkokl@gmail.com)
Build-Type: Simple
Cabal-Version: >= 1.14
Data-Files: SBVUnitTest/GoldFiles/*.gold
Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES
source-repository head
type: git
location: git://github.com/LeventErkok/sbv.git
Library
default-language: Haskell2010
ghc-options : -Wall
other-extensions: BangPatterns
-- Currently commented out since Cabal doesn't yet recognize DefaultSignatures extension yet. Uncomment when it does.
-- The current list can be seen at: https://github.com/haskell/cabal/blob/master/Cabal/Language/Haskell/Extension.hs
-- DefaultSignatures
DeriveDataTypeable
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GeneralizedNewtypeDeriving
MultiParamTypeClasses
OverlappingInstances
ParallelListComp
PatternGuards
Rank2Types
RankNTypes
ScopedTypeVariables
TupleSections
TypeOperators
TypeSynonymInstances
Build-Depends : base >= 4 && < 4.8
, array, containers, deepseq, directory, filepath, old-time
, pretty, process, mtl, QuickCheck, random, syb
Exposed-modules : Data.SBV
, Data.SBV.Internals
, Data.SBV.Examples.BitPrecise.BitTricks
, Data.SBV.Examples.BitPrecise.Legato
, Data.SBV.Examples.BitPrecise.MergeSort
, Data.SBV.Examples.BitPrecise.PrefixSum
, Data.SBV.Examples.CodeGeneration.AddSub
, Data.SBV.Examples.CodeGeneration.CRC_USB5
, Data.SBV.Examples.CodeGeneration.Fibonacci
, Data.SBV.Examples.CodeGeneration.GCD
, Data.SBV.Examples.CodeGeneration.PopulationCount
, Data.SBV.Examples.CodeGeneration.Uninterpreted
, Data.SBV.Examples.Crypto.AES
, Data.SBV.Examples.Crypto.RC4
, Data.SBV.Examples.Existentials.CRCPolynomial
, Data.SBV.Examples.Existentials.Diophantine
, Data.SBV.Examples.Polynomials.Polynomials
, Data.SBV.Examples.Puzzles.Coins
, Data.SBV.Examples.Puzzles.Counts
, Data.SBV.Examples.Puzzles.DogCatMouse
, Data.SBV.Examples.Puzzles.Euler185
, Data.SBV.Examples.Puzzles.MagicSquare
, Data.SBV.Examples.Puzzles.NQueens
, Data.SBV.Examples.Puzzles.Sudoku
, Data.SBV.Examples.Puzzles.U2Bridge
, Data.SBV.Examples.Uninterpreted.AUF
, Data.SBV.Examples.Uninterpreted.Deduce
, Data.SBV.Examples.Uninterpreted.Function
, Data.SBV.Examples.Uninterpreted.Sort
Other-modules : Data.SBV.BitVectors.AlgReals
, Data.SBV.BitVectors.Data
, Data.SBV.BitVectors.Model
, Data.SBV.BitVectors.PrettyNum
, Data.SBV.BitVectors.SignCast
, Data.SBV.BitVectors.Splittable
, Data.SBV.BitVectors.STree
, Data.SBV.Compilers.C
, Data.SBV.Compilers.CodeGen
, Data.SBV.SMT.SMT
, Data.SBV.SMT.SMTLib
, Data.SBV.SMT.SMTLib1
, Data.SBV.SMT.SMTLib2
, Data.SBV.Provers.Prover
, Data.SBV.Provers.SExpr
, Data.SBV.Provers.Yices
, Data.SBV.Provers.Z3
, Data.SBV.Tools.ExpectedValue
, Data.SBV.Tools.GenTest
, Data.SBV.Tools.Optimize
, Data.SBV.Tools.Polynomial
, Data.SBV.Utils.Boolean
, Data.SBV.Utils.TDiff
, Data.SBV.Utils.Lib
Executable SBVUnitTests
default-language: Haskell2010
ghc-options : -Wall
other-extensions: Rank2Types
RankNTypes
ScopedTypeVariables
TupleSections
Build-depends : base >= 4 && < 5
, HUnit, directory, filepath, process, sbv
Hs-Source-Dirs : SBVUnitTest
main-is : SBVUnitTest.hs
Other-modules : SBVUnitTestBuildTime
, SBVTest
, SBVTestCollection
, Examples.Arrays.Memory
, Examples.Basics.BasicTests
, Examples.Basics.Higher
, Examples.Basics.Index
, Examples.Basics.ProofTests
, Examples.Basics.QRem
, Examples.CRC.CCITT
, Examples.CRC.CCITT_Unidir
, Examples.CRC.GenPoly
, Examples.CRC.Parity
, Examples.CRC.USB5
, Examples.Puzzles.PowerSet
, Examples.Puzzles.Temperature
, Examples.Uninterpreted.Uninterpreted
, TestSuite.Arrays.Memory
, TestSuite.Basics.ArithNoSolver
, TestSuite.Basics.ArithSolver
, TestSuite.Basics.BasicTests
, TestSuite.Basics.Higher
, TestSuite.Basics.Index
, TestSuite.Basics.ProofTests
, TestSuite.Basics.QRem
, TestSuite.BitPrecise.BitTricks
, TestSuite.BitPrecise.Legato
, TestSuite.BitPrecise.MergeSort
, TestSuite.BitPrecise.PrefixSum
, TestSuite.CodeGeneration.AddSub
, TestSuite.CodeGeneration.CgTests
, TestSuite.CodeGeneration.CRC_USB5
, TestSuite.CodeGeneration.Fibonacci
, TestSuite.CodeGeneration.GCD
, TestSuite.CodeGeneration.PopulationCount
, TestSuite.CodeGeneration.Uninterpreted
, TestSuite.Crypto.AES
, TestSuite.Crypto.RC4
, TestSuite.Existentials.CRCPolynomial
, TestSuite.CRC.CCITT
, TestSuite.CRC.CCITT_Unidir
, TestSuite.CRC.GenPoly
, TestSuite.CRC.Parity
, TestSuite.CRC.USB5
, TestSuite.Puzzles.Coins
, TestSuite.Polynomials.Polynomials
, TestSuite.Puzzles.Counts
, TestSuite.Puzzles.DogCatMouse
, TestSuite.Puzzles.Euler185
, TestSuite.Puzzles.MagicSquare
, TestSuite.Puzzles.NQueens
, TestSuite.Puzzles.PowerSet
, TestSuite.Puzzles.Sudoku
, TestSuite.Puzzles.U2Bridge
, TestSuite.Puzzles.Temperature
, TestSuite.Uninterpreted.AUF
, TestSuite.Uninterpreted.Function
, TestSuite.Uninterpreted.Uninterpreted
Test-Suite SBVBasicTests
type : exitcode-stdio-1.0
default-language: Haskell2010
ghc-options : -Wall
Build-depends : base >= 4 && < 5
, HUnit, directory, filepath, sbv
Hs-Source-Dirs : SBVUnitTest
main-is : SBVBasicTests.hs
Other-modules : SBVBasicTests
, SBVTestCollection