@hackage sbv0.9.2

Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Categories
- Mathematics
License
BSD-3-Clause
Maintainer
Levent Erkok (erkokl@gmail.com)
Links
- Homepage
- Documentation
- No source repository
- Security
Versions
- 11.7 Fri, 16 May 2025
- 11.6 Sat, 10 May 2025
- 11.5 Fri, 25 Apr 2025
- 11.4 Thu, 13 Mar 2025
- 11.3 Mon, 10 Mar 2025
- 11.2 Sat, 8 Mar 2025

Installation
Custom
In your cabal file:
Dependencies (12)
- 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
Dependents (14)
@hackage/copilot-sbv, @hackage/crackNum, @hackage/cryptol, @hackage/verifiable-expressions, @hackage/sbv-program, @hackage/acme-everything, Show all…

Package Flags

test

(off by default)

Run the unit-test suite after build

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.

@hackage sbv0.9.2

Categories

License

Maintainer

Links

Versions

InstallationCustom

Dependencies (12)

Dependents (14)

Package Flags

Installation
Custom