[Haskell-cafe] [ANNOUNCE] New release of SBV (v8.1)
erkokl at gmail.com
Sun Mar 10 00:35:57 UTC 2019
Levent Erkok <erkokl at gmail.com>
Thu, Jul 20, 2017, 1:10 AM
I'm pleased to announce v8.1 release of SBV, a library for integrating SMT
solvers into Haskell.
This is a release with many new features. Some highlights:
* Support for symbolic sum-types: Maybe/Either. (Thanks to Joel Burget
for initiating these.)
* Support for symbolic sets.
* Support for uninterpreted-function values in models.
* Support for validation of models coming from SMT-solvers for
* An implementation of Dijkstra's weakest-precondition logic and a toy
language for showing how to do Hoare style total-correctness proofs in SBV.
* A new and better interface to the optimization engine supporting
arbitrary metric spaces.
* A bunch of other fixes, improvements, and examples.
Full release notes are here:
Feedback and bug reports are most welcome. Happy proving!
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe