The sbv package

[Tags: bsd3, library, program]

Adds support for symbolic bit vectors, allowing formal models of bit-precise programs to be created. Supports symbolic arrays and polynomials over GF(2^n). Aims to provide seamless integration with SMT solvers to produce formal property proofs of theoremhood and satisfiability, with counter-examples.


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, 3.2, 3.3, 3.4, 3.5, 4.0, 4.1, 4.2, 4.3, 4.4
Change logNone available
Dependenciesarray (>=0.2.0.0), base (>=3 && <5), containers (>=0.2.0), directory (>=1.0.1.1), filepath (>=1.1.0.4), haskell98, HUnit (>=1.2.2.3), mtl (>=1.1.0.2), old-time (>=1.0.0.2), parallel (>=2.2.0.1), process (>=1.0.1), QuickCheck (>=2.1.0.3), strict-concurrency (>=0.2.3)
LicenseBSD3
AuthorLevent Erkok
MaintainerLevent Erkok (erkokl@gmail.com)
StabilityExperimental
CategoryFormal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
Home pagehttp://github.com/LeventErkok/sbv
ExecutablesSBVUnitTests
UploadedSun Jan 16 09:38:21 UTC 2011 by LeventErkok
DistributionsLTSHaskell:4.2, NixOS:4.4, Stackage:4.4
Downloads7047 total (441 in last 30 days)
StatusDocs not available [build log]
All reported builds failed as of 2015-06-07 [all 2 reports]

Modules

Flags

NameDescriptionDefault
testRun the unit-test suite after buildDisabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees