SBV: SMT Based Verification in Haskell

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

$ ghci -XScopedTypeVariables
ghci> :m Data.SBV
ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
Q.E.D.
ghci> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
Falsifiable. Counter-example:
x = 128 :: SWord8

The function prove establishes theorem-hood, while sat finds any satisfying model. All satisfying models can be lazily computed using allSat.

Overview

• Latest release: v2.10 on Hackage. (Released: March 22, 2013.)
• Release Notes.
• 

SBV library provides support for dealing with symbolic values 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 like ordinary Haskell values when used concretely. However, when used with symbolic arguments, 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 for generating Haskell and C test vectors (the genTest function),
• compiled down to C, rendered as straight-line programs or libraries (compileToC and compileToCLib functions).

Picking the SMT solver to use

The SBV library uses third-party SMT solvers via the standard SMT-Lib interface. Use the following import statements to pick the corresponding solver:

• import Data.SBV.Bridge.Boolector
  Uses Boolector from Johannes Kepler University
• import Data.SBV.Bridge.CVC4
  Uses CVC4 from New York University and the University of Iowa.
• import Data.SBV.Bridge.Yices
  Uses Yices from SRI
• import Data.SBV.Bridge.Z3
  Uses Z3 from Microsoft

If you simply import Data.SBV, then the solver defaults to Microsoft's Z3.

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.

Copyright, License

The SBV library is distributed with the BSD3 license. See COPYRIGHT for details. The LICENSE file contains the BSD3 verbiage.

Thanks

The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Thomas DuBuisson, John Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.