Name: sbv Version: 0.9.17 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers. Automatically generate C programs from Haskell functions. The SBV library adds support for symbolic bit vectors, allowing formal models of bit-precise programs to be created. . > \$ ghci -XScopedTypeVariables > Prelude> :m Data.SBV > Prelude Data.SBV> prove \$ \(x::SWord8) -> x `shiftL` 2 .== 4*x > Q.E.D. > Prelude Data.SBV> prove \$ forAll ["x"] \$ \(x::SWord8) -> x `shiftL` 2 .== x > Falsifiable. Counter-example: > x = 128 :: SWord8 . The library introduces the following types and concepts: . * 'SBool': Symbolic Booleans (bits) . * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned) . * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed) . * 'SArray', 'SFunArray': Flat arrays of symbolic values . * Symbolic polynomials over GF(2^n), and polynomial arithmetic . * Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms . Predicates (i.e., functions that return 'SBool') built out of these types can be: . * proven correct via an external SMT solver (the 'prove' function) . * checked for satisfiability (the 'sat' and 'allSat' functions) . * quick-checked . The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs that can be executed in, say, embedded platforms. . In addition to the library, the installation will create the executable @SBVUnitTests@. You should run it once the installation is complete, to make sure the unit tests are run and all is well. . SBV is hosted at GitHub: . Comments, bug reports, and patches are always welcome. . Galois, Inc. () has contributed to the development of SBV, by providing time and computing machinery. The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Iavor Diatchki, Lee Pike, Don Stewart, and Josef Svenningsson. Copyright: Levent Erkok, 2010-2011 License: BSD3 License-file: LICENSE Stability: Experimental Author: Levent Erkok Homepage: http://github.com/LeventErkok/sbv Bug-reports: http://github.com/LeventErkok/sbv/issues Maintainer: Levent Erkok (erkokl@gmail.com) Build-Type: Custom Cabal-Version: >= 1.6 Data-Files: SBVUnitTest/GoldFiles/*.gold Extra-Source-Files: INSTALL, README, COPYRIGHT source-repository head type: git location: git://github.com/LeventErkok/sbv.git Library ghc-options : -Wall ghc-prof-options: -auto-all -caf-all Build-Depends : base >= 3 && < 5 , deepseq >= 1.1.0.2 , process >= 1.0.1.3 , containers >= 0.3.0.0 , QuickCheck >= 2.4.0.1 , strict-concurrency >= 0.2.4.1 , old-time >= 1.0.0.5 , mtl >= 2.0.1.0 , array >= 0.3.0.1 , HUnit >= 1.2.2.3 , directory >= 1.0.1.1 , filepath >= 1.1.0.4 , pretty >= 1.0.1.1 , random >= 1.0.0.2 Exposed-modules : Data.SBV , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato , Data.SBV.Examples.CodeGeneration.AddSub , Data.SBV.Examples.CodeGeneration.AES , Data.SBV.Examples.CodeGeneration.Fibonacci , Data.SBV.Examples.CodeGeneration.GCD , Data.SBV.Examples.CodeGeneration.PopulationCount , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.PrefixSum.PrefixSum , Data.SBV.Examples.Puzzles.DogCatMouse , Data.SBV.Examples.Puzzles.Euler185 , Data.SBV.Examples.Puzzles.MagicSquare , Data.SBV.Examples.Puzzles.NQueens , Data.SBV.Examples.Puzzles.Sudoku , Data.SBV.Examples.Puzzles.U2Bridge , Data.SBV.Examples.Uninterpreted.AUF , Data.SBV.Examples.Uninterpreted.Function Other-modules : Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Model , Data.SBV.BitVectors.Splittable , Data.SBV.BitVectors.Polynomial , Data.SBV.BitVectors.PrettyNum , Data.SBV.Compilers.C , Data.SBV.Compilers.CodeGen , Data.SBV.SMT.SMT , Data.SBV.SMT.SMTLib , Data.SBV.Provers.Prover , Data.SBV.Provers.SExpr , Data.SBV.Provers.Yices , Data.SBV.Utils.Boolean , Data.SBV.Utils.TDiff , Data.SBV.Utils.SBVTest , Data.SBV.Utils.Lib , Data.SBV.Examples.Arrays.Memory , Data.SBV.Examples.Basics.BasicTests , Data.SBV.Examples.Basics.Higher , Data.SBV.Examples.Basics.Index , Data.SBV.Examples.Basics.ProofTests , Data.SBV.Examples.Basics.QRem , Data.SBV.Examples.CRC.CCITT , Data.SBV.Examples.CRC.CCITT_Unidir , Data.SBV.Examples.CRC.GenPoly , Data.SBV.Examples.CRC.Parity , Data.SBV.Examples.CRC.USB5 , Data.SBV.Examples.Puzzles.PowerSet , Data.SBV.Examples.Puzzles.Temperature , Data.SBV.Examples.Uninterpreted.Uninterpreted , Data.SBV.TestSuite.Arrays.Memory , Data.SBV.TestSuite.Basics.Arithmetic , Data.SBV.TestSuite.Basics.BasicTests , Data.SBV.TestSuite.Basics.Higher , Data.SBV.TestSuite.Basics.Index , Data.SBV.TestSuite.Basics.ProofTests , Data.SBV.TestSuite.Basics.QRem , Data.SBV.TestSuite.BitPrecise.BitTricks , Data.SBV.TestSuite.BitPrecise.Legato , Data.SBV.TestSuite.CodeGeneration.AddSub , Data.SBV.TestSuite.CodeGeneration.AES , Data.SBV.TestSuite.CodeGeneration.CgTests , Data.SBV.TestSuite.CodeGeneration.Fibonacci , Data.SBV.TestSuite.CodeGeneration.GCD , Data.SBV.TestSuite.CodeGeneration.PopulationCount , Data.SBV.TestSuite.CRC.CCITT , Data.SBV.TestSuite.CRC.CCITT_Unidir , Data.SBV.TestSuite.CRC.GenPoly , Data.SBV.TestSuite.CRC.Parity , Data.SBV.TestSuite.CRC.USB5 , Data.SBV.TestSuite.PrefixSum.PrefixSum , Data.SBV.TestSuite.Polynomials.Polynomials , Data.SBV.TestSuite.Puzzles.DogCatMouse , Data.SBV.TestSuite.Puzzles.Euler185 , Data.SBV.TestSuite.Puzzles.MagicSquare , Data.SBV.TestSuite.Puzzles.NQueens , Data.SBV.TestSuite.Puzzles.PowerSet , Data.SBV.TestSuite.Puzzles.Sudoku , Data.SBV.TestSuite.Puzzles.U2Bridge , Data.SBV.TestSuite.Puzzles.Temperature , Data.SBV.TestSuite.Uninterpreted.AUF , Data.SBV.TestSuite.Uninterpreted.Uninterpreted , Data.SBV.TestSuite.Uninterpreted.Function Executable SBVUnitTests main-is : SBVUnitTest/SBVUnitTest.hs