The sbv package

Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers. Automatically generate C programs from Haskell functions. The SBV library adds support for symbolic bit vectors, allowing formal models of bit-precise 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)
SArray, SFunArray: Flat arrays of symbolic values
Symbolic polynomials over GF(2^n), and polynomial arithmetic
Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms

Predicates (i.e., functions that return SBool) 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)
quick-checked

The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs that can be executed in, say, embedded platforms.

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.

Galois, Inc. (http://www.galois.com) has contributed to the development of SBV, by providing time and computing machinery. The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Iavor Diatchki, Lee Pike, Don Stewart, and Josef Svenningsson.

Properties

Versions	0.9, 0.9.1, 0.9.2, 0.9.3, 0.9.4, 0.9.5, 0.9.6, 0.9.7, 0.9.8, 0.9.9, 0.9.10, 0.9.11, 0.9.12, 0.9.13, 0.9.14, 0.9.15, 0.9.16, 0.9.17, 0.9.18, 0.9.19, 0.9.20, 0.9.21, 0.9.22, 0.9.23, 0.9.24, 1.0, 1.1, 1.2, 1.3, 1.4, 2.0, 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10
Dependencies	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), HUnit (≥1.2.2.3), 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.0.2), strict-concurrency (≥0.2.4.1)
License	BSD3
Copyright	Levent Erkok, 2011
Author	Levent Erkok
Maintainer	Levent Erkok (erkokl@gmail.com)
Stability	Experimental
Category	Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
Home page	http://github.com/LeventErkok/sbv
Bug tracker	http://github.com/LeventErkok/sbv/issues
Source repository	git clone git://github.com/LeventErkok/sbv.git
Executables	SBVUnitTests
Upload date	Sun Mar 20 01:52:51 UTC 2011
Uploaded by	LeventErkok
Built on	ghc-7.0

Modules

Data
- Data.SBV
  - Examples
  - Data.SBV.Internals

Downloads

sbv-0.9.14.tar.gz (Cabal source package)
package description (included in the package)