sbv
Version 0.9.19 revision 0 uploaded by LeventErkok.
Package meta
- Synopsis
- Symbolic bit vectors: Bit-precise verification and automatic C-code generation.
- Description
Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers. Automatically generate C programs from Haskell functions. The SBV library adds support for symbolic bit vectors, allowing formal models of bit-precise programs to be created.
$ ghci -XScopedTypeVariables Prelude> :m Data.SBV Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x Q.E.D. Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x Falsifiable. Counter-example: x = 128 :: SWord8
The library introduces the following types and concepts:
SBool: Symbolic Booleans (bits)
SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned)
STree: Full binary trees of symbolic values (for fast symbolic access)
Symbolic polynomials over GF(2^n), and polynomial arithmetic
Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms
Predicates (i.e., functions that return SBool) built out of these types can be:
proven correct via an external SMT solver (the prove function)
quick-checked
The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs.
In addition to the library, the installation will create the executable
SBVUnitTests
. You should run it once the installation is complete, to make sure the unit tests are run and all is well.SBV is hosted at GitHub: http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.
Galois, Inc. (http://www.galois.com) has contributed to the development of SBV, by providing time and computing machinery. The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson.
- Author
- Levent Erkok
- Bug reports
- http://github.com/LeventErkok/sbv/issues
- Category
- Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
- Copyright
- Levent Erkok, 2010-2011
- Homepage
- http://github.com/LeventErkok/sbv
- Maintainer
- Levent Erkok (erkokl@gmail.com)
- Package URL
- n/a
- Stability
- Experimental