# sbvPlugin: Formally prove properties of Haskell programs using SBV/SMT

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

GHC plugin for proving properties over Haskell functions using SMT solvers, based on the SBV package.

See Data.SBV.Plugin for a quick example, or the modules under `Data.SBV.Plugin.Examples`

for more details.

[Skip to Readme]

Versions [faq] | 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 0.10, 0.11, 0.12 (info) |
---|---|

Change log | CHANGES.md |

Dependencies | base (>=4.11 && <5), containers, ghc, ghc-prim, mtl, sbv (>=8.8), template-haskell [details] |

License | BSD-3-Clause |

Author | Levent Erkok |

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

Category | Formal methods, Theorem provers, Math, SMT, Symbolic Computation |

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

Bug tracker | http://github.com/LeventErkok/sbvPlugin/issues |

Source repo | head: git clone git://github.com/LeventErkok/sbvPlugin.git |

Uploaded | by LeventErkok at 2020-09-05T21:54:56Z |

Distributions | NixOS:0.12 |

Downloads | 4681 total (21 in the last 30 days) |

Rating | (no votes yet) [estimated by Bayesian average] |

Your Rating | |

Status | Docs not available [build log] All reported builds failed as of 2020-09-05 [all 3 reports] |

## Modules

*Data**SBV*- Data.SBV.Plugin
- Data.SBV.Plugin.Data
*Examples*- Data.SBV.Plugin.Examples.BitTricks
- Data.SBV.Plugin.Examples.MergeSort
- Data.SBV.Plugin.Examples.MicroController

- Data.SBV.Plugin

## Downloads

- sbvPlugin-0.12.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)