SBV

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

View the Project on GitHub

SBV: SMT Based Verification in Haskell

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

$ ghci
ghci> :m Data.SBV
ghci> prove $ \x -> x `shiftL` 2 .== 4 * (x::SWord8)
Q.E.D.
ghci> prove $ \x -> x `shiftL` 2 .== 2 * (x::SWord8)
Falsifiable. Counter-example:
  s0 = 32 :: Word8

The function prove establishes theorem-hood, while sat finds any satisfying model. All satisfying models can be lazily computed using allSat. SBV can also perform static assertion checks, such as absence of division-by-0, and other user given properties.

Overview

SBV library provides support for dealing with symbolic values in Haskell. It introduces the types:

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:

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:

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

See versions for a listing of the versions of these tools SBV has been tested with. Please report if you see any discrepancies!

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.

Using multiple solvers, simultaneously

SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. See proveWithAny/proveWithAll and satWithAny/satWithAll functions. The function sbvAvailableSolvers can be used to query the available solvers at run-time.

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: Reid Barton, Ian Blumenfeld, Ian Calvert, Christian Conkle, Iavor Diatchki, Robert Dockins, Thomas DuBuisson, Trevor Elliott, John Erickson, Adam Foltzer, Tom Hawkins, Brian Huffman, Joe Leslie-Hurd, Georges-Axel Jaloyan, Tom Sydney Kerckhove, Piërre van de Laar, Brett Letner, Philipp Meyer, Lee Pike, Stephan Renatus, Eric Seidel, Austin Seipp, Andrés Sicard-Ramírez, Don Stewart, Josef Svenningsson, Daniel Wagner, Sean Weaver, Nis Wegmann, and Jared Ziegler.