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

# sbv-5.14: 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.

For details, please see: http://leventerkok.github.com/sbv/

Modules

- Data
  - Data.SBV
    - Bridge
      - Data.SBV.Bridge.ABC
      - Data.SBV.Bridge.Boolector
      - Data.SBV.Bridge.CVC4
      - Data.SBV.Bridge.MathSAT
      - Data.SBV.Bridge.Yices
      - Data.SBV.Bridge.Z3
    - Data.SBV.Dynamic
    - Examples
      - BitPrecise
        - Data.SBV.Examples.BitPrecise.BitTricks
        - Data.SBV.Examples.BitPrecise.Legato
        - Data.SBV.Examples.BitPrecise.MergeSort
        - Data.SBV.Examples.BitPrecise.MultMask
        - Data.SBV.Examples.BitPrecise.PrefixSum
      - CodeGeneration
        - Data.SBV.Examples.CodeGeneration.AddSub
        - Data.SBV.Examples.CodeGeneration.CRC_USB5
        - Data.SBV.Examples.CodeGeneration.Fibonacci
        - Data.SBV.Examples.CodeGeneration.GCD
        - Data.SBV.Examples.CodeGeneration.PopulationCount
        - Data.SBV.Examples.CodeGeneration.Uninterpreted
      - Crypto
        - Data.SBV.Examples.Crypto.AES
        - Data.SBV.Examples.Crypto.RC4
      - Existentials
        - Data.SBV.Examples.Existentials.CRCPolynomial
        - Data.SBV.Examples.Existentials.Diophantine
      - Misc
        - Data.SBV.Examples.Misc.Auxiliary
        - Data.SBV.Examples.Misc.Enumerate
        - Data.SBV.Examples.Misc.Floating
        - Data.SBV.Examples.Misc.ModelExtract
        - Data.SBV.Examples.Misc.NoDiv0
        - Data.SBV.Examples.Misc.Word4
      - Polynomials
        - Data.SBV.Examples.Polynomials.Polynomials
      - Puzzles
        - Data.SBV.Examples.Puzzles.Birthday
        - Data.SBV.Examples.Puzzles.Coins
        - Data.SBV.Examples.Puzzles.Counts
        - Data.SBV.Examples.Puzzles.DogCatMouse
        - Data.SBV.Examples.Puzzles.Euler185
        - Data.SBV.Examples.Puzzles.Fish
        - Data.SBV.Examples.Puzzles.MagicSquare
        - Data.SBV.Examples.Puzzles.NQueens
        - Data.SBV.Examples.Puzzles.SendMoreMoney
        - Data.SBV.Examples.Puzzles.Sudoku
        - Data.SBV.Examples.Puzzles.U2Bridge
      - Uninterpreted
        - Data.SBV.Examples.Uninterpreted.AUF
        - Data.SBV.Examples.Uninterpreted.Deduce
        - Data.SBV.Examples.Uninterpreted.Function
        - Data.SBV.Examples.Uninterpreted.Shannon
        - Data.SBV.Examples.Uninterpreted.Sort
        - Data.SBV.Examples.Uninterpreted.UISortAllSat
    - Data.SBV.Internals