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

[ bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ]
[ Propose Tags ]

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.

[Skip to Readme]

Versions [faq] | 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, 3.0, 3.1, 3.2, 3.3, 3.4, 3.5, 4.0, 4.1, 4.2, 4.3, 4.4, 5.0, 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 5.8, 5.9, 5.10, 5.11, 5.12, 5.13, 5.14, 5.15, 6.0, 6.1, 7.0, 7.1, 7.2, 7.3, 7.4, 7.5, 7.6, 7.7, 7.8, 7.9, 7.10, 7.11, 7.12, 7.13, 8.0, 8.1, 8.2, 8.3, 8.4, 8.5, 8.6, 8.7, 8.8, 8.9, 8.10 (info) |
---|---|

Dependencies | array (>=0.2.0.0), base (>=3 && <5), containers (>=0.2.0), directory (>=1.0.1.1), filepath (>=1.1.0.4), haskell98 (<1.2), HUnit (>=1.2.2.3), mtl (>=1.1.0.2), old-time (>=1.0.0.2), parallel (>=2.2.0.1), process (>=1.0.1), QuickCheck (>=2.1.0.3 && <2.3), strict-concurrency (>=0.2.3) [details] |

License | BSD-3-Clause |

Author | Levent Erkok |

Maintainer | Levent Erkok (erkokl@gmail.com) |

Revised | Revision 1 made by HerbertValerioRiedel at 2018-10-03T09:16:41Z |

Category | Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math |

Home page | http://github.com/LeventErkok/sbv |

Uploaded | by LeventErkok at 2011-01-16T09:38:21Z |

Distributions | Arch:8.10, Debian:7.12, LTSHaskell:7.13, NixOS:8.9, Stackage:8.3 |

Executables | SBVUnitTests |

Downloads | 54703 total (1366 in the last 30 days) |

Rating | 2.75 (votes: 9) [estimated by Bayesian average] |

Your Rating | |

Status | Docs not available [build log] All reported builds failed as of 2016-12-28 [all 7 reports] |

## Modules

*Data*- Data.SBV
*Examples**BitPrecise*- Data.SBV.Examples.BitPrecise.BitTricks
- Data.SBV.Examples.BitPrecise.Legato

*Puzzles*- Data.SBV.Examples.Puzzles.DogCatMouse
- Data.SBV.Examples.Puzzles.MagicSquare
- Data.SBV.Examples.Puzzles.NQueens
- Data.SBV.Examples.Puzzles.Sudoku
- Data.SBV.Examples.Puzzles.U2Bridge

- Data.SBV.Internals

- Data.SBV

## Flags

Name | Description | Default | Type |
---|---|---|---|

test | Run the unit-test suite after build | Disabled | Automatic |

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

## Downloads

- sbv-0.9.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.