The sbv package
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
| Versions | 0.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 |
|---|---|
| Dependencies | array (≥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) |
| License | BSD3 |
| Copyright | Levent Erkok, 2011 |
| Author | Levent Erkok |
| Maintainer | Levent Erkok (erkokl@gmail.com) |
| Stability | Experimental |
| Category | Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math |
| Home page | http://github.com/LeventErkok/sbv |
| Executables | SBVUnitTests |
| Upload date | Tue Jan 18 08:38:18 UTC 2011 |
| Uploaded by | LeventErkok |
| Built on | ghc-7.0 |
Modules
- Data
- Data.SBV
- Examples
- BitPrecise
- Polynomials
- Puzzles
- Uninterpreted
- Data.SBV.Internals
- Examples
- Data.SBV
Downloads
- sbv-0.9.6.tar.gz (Cabal source package)
- package description (included in the package)