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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

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

Levent Erkok

Levent Erkok <[hidden email]>

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.



Feedback and bug reports are most welcome. Happy proving!

-Levent.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.