sbv-1.4: sbv.cabal
Name: sbv
Version: 1.4
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 library 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 SMT-Lib 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: <http://github.com/LeventErkok/sbv>. 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: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>.
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.8
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
ghc-options : -Wall
Build-Depends : array >= 0.3.0.1
, base >= 3 && < 5
, containers >= 0.3.0.0
, deepseq >= 1.1.0.2
, directory >= 1.0.1.1
, filepath >= 1.1.0.4
, mtl >= 2.0.1.0
, old-time >= 1.0.0.5
, pretty >= 1.0.1.1
, process >= 1.0.1.3
, QuickCheck >= 2.4.0.1
, random >= 1.0.1.1
, strict-concurrency >= 0.2.4.1
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.Function
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
ghc-options : -Wall
Build-depends : base >= 3 && < 5
, directory >= 1.0.1.1
, HUnit >= 1.2.4.2
, filepath >= 1.1.0.4
, process >= 1.0.1.3
, sbv
Hs-Source-Dirs : SBVUnitTest
main-is : SBVUnitTest.hs
Other-modules : SBVUnitTestBuildTime
, SBVTest
, 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.Arithmetic
, TestSuite.Basics.BasicTests
, TestSuite.Basics.Higher
, TestSuite.Basics.Index
, TestSuite.Basics.ProofTests
, TestSuite.Basics.QRem
, TestSuite.BitPrecise.BitTricks
, TestSuite.BitPrecise.Legato
, 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