@hackage sbv0.9.10

Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers. 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

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.