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

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 valuesSymbolic 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.

[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 (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), 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) [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 |

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 Tue Mar 29 19:15:51 UTC 2011 |

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

Executables | SBVUnitTests |

Downloads | 35210 total (624 in the last 30 days) |

Rating | 2.75 (votes: 9) [estimated by rule of succession] |

Your Rating | |

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

## Modules

[Index]

*Data*- Data.SBV
*Examples**BitPrecise**CodeGeneration**Polynomials**PrefixSum**Puzzles**Uninterpreted*

- Data.SBV.Internals

- Data.SBV

## Downloads

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