SBV: SMT Based Verification in Haskell
Express properties about 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
prove has the following type:
prove :: Provable a => a -> IO ThmResult
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 (
allSat) are also provided.
In addition, functions using the SBV library can be compiled to C automatically.
The SBV library is hosted at http://github.com/LeventErkok/sbv.
The hackage site 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.
The Haskell SBV library provides support for dealing with Symbolic Bit Vectors in Haskell. It introduces the types:
SBool: Symbolic Booleans (bits).
SWord64: Symbolic Words (unsigned).
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
Bits, (custom versions of)
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
- checked for satisfiability (the
- used in synthesis (the
satfunction with existentials)
- optimized with respect to cost functions (the
- used in concrete test case generation (the
genTestfunction), rendered as values in various languages, including Haskell and C.
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/.
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.
You should have at least one of Z3 (download), or Yices (download) (version 2.X) 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
(The default for the latter is
"-m -f"). Similarly the environment variables
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.)
Please see the files under the 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.
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 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.
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.