Data.SBV

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

Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.SBV

Contents

Symbolic types
- Booleans
  - Boolean values and functions
  - Logical aggregations
- Bit-vectors
- Unbounded integers
- Floating point numbers
- Rationals
- Algebraic reals
- Characters, Strings and Regular Expressions
- Symbolic lists
- Tuples
- Sum types
- Sets
Arrays of symbolic values
Creating symbolic values
- Single value
- List of values
Symbolic Equality and Comparisons
Conditionals: Mergeable values
Symbolic integral numbers
Division and Modulus
Bit-vector operations
- Conversions
- Shifts and rotates
- Finite bit-vector operations
- Splitting, joining, and extending bit-vectors
- Exponentiation
IEEE-floating point numbers
- Rounding modes
- Conversion to/from floats
- Bit-pattern conversions
- Extracting bit patterns from floats
- Showing values in detail
Enumerations
Uninterpreted sorts, constants, and functions
Stopping unrolling: Defined functions
Special relations
Properties, proofs, and satisfiability
Constraints and Quantifiers
- Quantified constraints, quantifier elimination, and skolemization
- Constraint Vacuity
- Named constraints and attributes
- Unsat cores
- Cardinality constraints
Checking safety
Quick-checking
Optimization
- Multiple optimization goals
- Objectives and Metrics
- Soft assertions
- Field extensions
Model extraction
- Inspecting proof results
- Observing expressions
- Programmable model extraction
SMT Interface
- Controlling verbosity
- Solvers
- Configurations
- SBV exceptions
Abstract SBV type
Module exports

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: SMT Based Verification

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

>>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.

>>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
Falsifiable. Counter-example:
  s0 = 64 :: Word8

And similarly, sat finds a satisfying instance. The types involved are:

    prove :: Provable a => a -> IO ThmResult
    sat   :: Satisfiable a => a ->