[Haskell-cafe] [ANNOUNCE] New release of SBV (v8.1)

[Levent Erkok]

Levent Erkok <erkokl at gmail.com>
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190309/2ecefcfa/attachment.html>