# sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers. Automatically generate C programs from Haskell functions. The SBV library adds support for symbolic bit vectors and other symbolic types, allowing formal models of Haskell 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 SBV library uses Microsoft's Z3 SMT solver (http://research.microsoft.com/en-us/um/redmond/projects/z3/) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (http://yices.csl.sri.com/download-yices2.shtml), although the Z3 binding is much more richer.

SBV 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)

• SReal: Symbolic algebraic reals (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 axioms.

• Uninterpreted sorts, and proofs over such sorts, potentially with 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, John Erickson, 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.

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) array, base (==4.*), containers, deepseq, directory, filepath, HUnit, mtl, old-time, pretty, process, QuickCheck, random, sbv, syb [details] BSD-3-Clause Levent Erkok, 2010-2012 Levent Erkok Levent Erkok (erkokl@gmail.com) Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT http://github.com/LeventErkok/sbv http://github.com/LeventErkok/sbv/issues head: git clone git://github.com/LeventErkok/sbv.git by LeventErkok at 2012-11-29T03:31:32Z Arch:8.8, Debian:7.12, LTSHaskell:7.13, NixOS:8.8, Stackage:8.3 SBVUnitTests 51154 total (405 in the last 30 days) 2.75 (votes: 9) [estimated by Bayesian average] λ λ λ Docs uploaded by userBuild status unknown

#### Maintainer's Corner

For package maintainers and hackage trustees

[back to package description]
SBV: SMT Based Verification in Haskell
======================================

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

haskell
$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:

haskell
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.
In addition, functions using the SBV library can be compiled to C automatically.

Build Status
============
SBV uses Travis-CI's automated build infrastructure, making a build for each commit. Current build status:
[![Build Status](https://secure.travis-ci.org/LeventErkok/sbv.png?branch=master)](http://travis-ci.org/LeventErkok/sbv)

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

The hackage site
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).
- SInteger: Symbolic unbounded integers (signed).
- SReal: Symbolic infinite precision algebraic reals (signed).
- Arrays of symbolic values.
- Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs.
- Uninterpreted constants and functions over symbolic values, with user defined axioms.
- Uninterpreted sorts, and proofs over such sorts, potentially with 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, functions 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)
- used in synthesis (the sat function with existentials)
- 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

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.

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

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/).

Currently, we fully support the
[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,
and the [Yices](http://yices.csl.sri.com) SMT solver from SRI. Both solvers are available
for Windows, Linux, and Mac OSX.

Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please
do get in touch if you plan to use SBV with any other solver.

Prerequisites
=============
You **should** have at least one of
installed on your machine, preferably both. Note that z3 is the default solver used by 'sat',
'allSat', 'prove', etc. commands. To use "yices", use the 'satWith', 'proveWith', 'allSatWith' variants.

Make sure the executables for the solvers are in your path. Alternatively, you can specify the location
of the 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"). Similarly the environment variables SBV_Z3 and SBV_Z3_OPTIONS can
be used for choosing executable location and custom options for Z3.  (The default for the latter is
"/in /smt2" on Windows and "-in -smt2" on Mac and Linux. You should use Z3 version 4.1 or later.)

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.