Levent Erkok
Thu, Jul 20, 2017, 1:10 AM
to Haskell
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
high-assurance.
* 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:
https://github.com/LeventErkok/sbv/blob/master/CHANGES.md
Hackage: https://hackage.haskell.org/package/sbv
Homepage: http://leventerkok.github.io/sbv/
Feedback and bug reports are most welcome. Happy proving!
-Levent.
