sbv

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/

SBV: SMT Based Verification in Haskell

Please see: http://leventerkok.github.io/sbv/

Build Status

• Linux:
  • GHC 8.2.2
  • GHC 8.4.3
• Mac OSX:
  • GHC 8.4.3
• Windows:
  • GHC 8.4.3