sbv: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

[ bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ] [ Propose Tags ]
This version is deprecated.

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.


[Skip to Readme]

Modules

[Last Documentation]

  • Data
    • Data.SBV
      • Examples
        • BitPrecise
          • Data.SBV.Examples.BitPrecise.BitTricks
          • Data.SBV.Examples.BitPrecise.Legato
        • Polynomials
          • Data.SBV.Examples.Polynomials.Polynomials
        • PrefixSum
          • Data.SBV.Examples.PrefixSum.PrefixSum
        • Puzzles
          • 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
        • Uninterpreted
          • Data.SBV.Examples.Uninterpreted.AUF
          • Data.SBV.Examples.Uninterpreted.Function
      • Data.SBV.Internals

Flags

Automatic Flags
NameDescriptionDefault
test

Run the unit-test suite after build

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 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, 3.0, 3.1, 3.2, 3.3, 3.4, 3.5, 4.0, 4.1, 4.2, 4.3, 4.4, 5.0, 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 5.8, 5.9, 5.10, 5.11, 5.12, 5.13, 5.14, 5.15, 6.0, 6.1, 7.0, 7.1, 7.2, 7.3, 7.4, 7.5, 7.6, 7.7, 7.8, 7.9, 7.10, 7.11, 7.12, 7.13, 8.0, 8.1, 8.2, 8.3, 8.4, 8.5, 8.6, 8.7, 8.8, 8.9, 8.10, 8.11, 8.12, 8.13, 8.14, 8.15, 8.16, 8.17, 9.0, 9.1, 9.2, 10.0, 10.1, 10.2, 10.3, 10.4, 10.5, 10.6 (info)
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), process (>=1.0.1.3), QuickCheck (>=2.4.0.1), strict-concurrency (>=0.2.4.1) [details]
License BSD-3-Clause
Copyright Levent Erkok, 2011
Author Levent Erkok
Maintainer Levent Erkok (erkokl@gmail.com)
Category Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
Home page http://github.com/LeventErkok/sbv
Source repo head: git clone git://github.com/LeventErkok/sbv.git
Uploaded by LeventErkok at 2011-02-16T07:07:05Z
Distributions Arch:9.1, Debian:8.7, LTSHaskell:10.2, Stackage:10.5
Reverse Dependencies 12 direct, 11 indirect [details]
Executables SBVUnitTests
Downloads 74960 total (377 in the last 30 days)
Rating 2.75 (votes: 9) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-28 [all 7 reports]

Readme for sbv-0.9.10

[back to package description]
SBV: Symbolic Bit Vectors in Haskell
====================================

Express properties about bit-precise Haskell programs and automatically prove
them using SMT solvers.

        $ 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 function `prove` has the following type:
    
        prove :: Provable a => a -> IO ThmResult

The class `Provable` comes with instances for n-ary predicates, for arbitrary n.
The predicates are just regular Haskell functions over symbolic signed and unsigned
bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided.

Resources
=========
The sbv library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).

The hackage site
[http://hackage.haskell.org/package/sbv](http://hackage.haskell.org/package/sbv) is the best place
for details on the API and the example use cases.

Comments, bug reports, and patches are always welcome.

Overview
========
The Haskell sbv library provides support for dealing with Symbolic Bit Vectors
in Haskell. It introduces the types:

  - `SBool`: Symbolic Booleans (bits)
  - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned)
  - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed)
  - 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

The user can construct ordinary Haskell programs using these types, which behave
very similar to their concrete counterparts. In particular these types belong to the
standard classes `Num`, `Bits`, (custom versions of) `Eq` and `Ord`, along with several
other custom classes for simplifying bit-precise programming with symbolic values. The
framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return `SBool`) built out of these types can also be:

  - proven correct via an external SMT solver (the `prove` function)
  - checked for satisfiability (the `sat` and `allSat` functions)
  - quick-checked

If a predicate is not valid, `prove` will return a counterexample: An 
assignment to inputs such that the predicate fails. The `sat` function will
return a satisfying assignment, if there is one. The `allSat` function returns
all satisfying assignments, lazily.

Use of SMT solvers
==================
The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: 
[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/)

While the library is designed to work with any SMT-Lib compliant SMT-solver,
solver specific support is required for parsing counter-example/model data since
there is currently no agreed upon format for getting models from arbitrary SMT
solvers. (The SMT-Lib2 initiative will potentially address this issue in the
future, at which point the sbv library can be generalized as well.) Currently, we
only support the Yices SMT solver from SRI as far as the counter-example
and model generation support is concerned:
[http://yices.csl.sri.com/](http://yices.csl.sri.com/) However, other solvers can
be hooked up with relative ease.

Prerequisites
=============
You **should** download and install Yices (version 2.X) on your machine, and
make sure the "yices" executable is in your path before using the sbv library,
as it is the current default solver. Alternatively, you can specify the location
of yices executable in the environment variable `SBV_YICES` and the options to yices
in `SBV_YICES_OPTIONS`. (The default for the latter is `"-m -f"`.)

Examples
=========
Please see the files under the
[Examples](http://github.com/LeventErkok/sbv/tree/master/Data/SBV/Examples)
directory for a number of interesting applications and use cases. Amongst others,
it contains solvers for Sudoku and N-Queens puzzles as mandatory SMT solver examples in
the Puzzles directory.

Installation
============
The sbv library is cabalized. Assuming you have cabal/ghc installed, it should merely
be a matter of running 
     
         cabal install sbv
	 
Please see [INSTALL](http://github.com/LeventErkok/sbv/tree/master/INSTALL) for installation details.

Once the installation is done, you can run the executable `SBVUnitTests` which will
execute the regression test suite for sbv on your machine to ensure all is well.

Copyright, License
==================
The sbv library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for
details. The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains
the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.