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
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
Upload dateSun Jan 16 09:38:21 UTC 2011
Uploaded byLeventErkok
DistributionsNixOS:3.1
Downloads3330 total (257 in last 30 days)

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