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). Supports uninterpreted constants and functions. 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
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 dateMon Jan 17 11:03:09 UTC 2011
Uploaded byLeventErkok
DistributionsNixOS:3.2
Downloads3847 total (415 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