The sbv package

[Tags: bsd3, library, program]

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:

Predicates (i.e., functions that return SBool) built out of these types can be:

The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs.

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: http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.

Galois, Inc. (http://www.galois.com) 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: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson.


Properties

Versions0.9, 0.9.1, 0.9.2, 0.9.3, 0.9.4, 0.9.5, 0.9.6, 0.9.7, 0.9.8, 0.9.9, 0.9.10, 0.9.11, 0.9.12, 0.9.13, 0.9.14, 0.9.15, 0.9.16, 0.9.17, 0.9.18, 0.9.19, 0.9.20, 0.9.21, 0.9.22, 0.9.23, 0.9.24, 1.0, 1.1, 1.2, 1.3, 1.4, 2.0, 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10, 3.0, 3.1
Dependenciesarray (>=0.3.0.1), base (>=3 && <5), containers (>=0.3.0.0), deepseq (>=1.1.0.2), directory (>=1.0.1.1), filepath (>=1.1.0.4), HUnit (>=1.2.2.3), mtl (>=2.0.1.0), old-time (>=1.0.0.5), pretty (>=1.0.1.1), process (>=1.0.1.3), QuickCheck (>=2.4.0.1), random (>=1.0.0.2), strict-concurrency (>=0.2.4.1)
LicenseBSD3
CopyrightLevent Erkok, 2010-2011
AuthorLevent Erkok
MaintainerLevent Erkok (erkokl@gmail.com)
StabilityExperimental
CategoryFormal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
Home pagehttp://github.com/LeventErkok/sbv
Bug trackerhttp://github.com/LeventErkok/sbv/issues
Source repositoryhead: git clone git://github.com/LeventErkok/sbv.git
ExecutablesSBVUnitTests
Upload dateMon Jun 6 00:53:59 UTC 2011
Uploaded byLeventErkok
DistributionsNixOS:3.1
Downloads3381 total (303 in last 30 days)

Modules

[Index]

Downloads

Maintainers' corner

For package maintainers and hackage trustees