# sbv: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.

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)`SInteger`

: Symbolic unbounded integers (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, 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.

[Skip to Readme]

Versions [faq] | 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 (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.4.2), 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) [details] |

License | BSD-3-Clause |

Copyright | Levent Erkok, 2010-2011 |

Author | Levent Erkok |

Maintainer | Levent Erkok (erkokl@gmail.com) |

Category | Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT |

Home page | http://github.com/LeventErkok/sbv |

Bug tracker | http://github.com/LeventErkok/sbv/issues |

Source repo | head: git clone git://github.com/LeventErkok/sbv.git |

Uploaded | by LeventErkok at 2012-02-15T03:36:10Z |

Distributions | Arch:8.8, Debian:7.12, LTSHaskell:7.13, NixOS:8.8, Stackage:8.3 |

Executables | SBVUnitTests |

Downloads | 50683 total (1364 in the last 30 days) |

Rating | 2.75 (votes: 9) [estimated by Bayesian average] |

Your Rating | |

Status | Docs uploaded by user Build status unknown [no reports yet] |

## Modules

[Index]

*Data*- Data.SBV
*Examples**BitPrecise**CodeGeneration**Crypto**Existentials**Polynomials**Puzzles**Uninterpreted*

- Data.SBV.Internals

- Data.SBV

## Downloads

- sbv-1.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)