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.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), process (>=1.0.1.3), QuickCheck (>=2.4.0.1), strict-concurrency (>=0.2.4.1)
LicenseBSD3
CopyrightLevent Erkok, 2011
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 21:00:47 UTC 2011
Uploaded byLeventErkok
DistributionsNixOS:3.1
Downloads2671 total (338 in last 30 days)

Modules

[Index]

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