[Haskell] [ANNOUNCE] New release of SBV

[Levent Erkok]

I'm happy to announce a new release of SBV (v4.0); a library for seamlessly
integrating SMT solvers with Haskell.

       https://hackage.haskell.org/package/sbv

Most of the changes in this release are due to Brian Huffman of Galois;
essentially adding capabilities so end-users can define symbolic bit-vector
types that are not natively supported by SBV. For instance, a user can
define `SWord17` for representing 17-bit words and use them just like other
symbolic types natively supported by SBV. This feature allows SBV to take
advantage of arbitrary bit-size decision procedures for bit-vector logics
as found in modern SMT solvers, which are becoming increasingly more
valuable in (semi-)automated verification of software artifacts. (Note that
SBV already supports other basic types such as unbounded Integers, IEEE
Floats and Doubles, Rationals, Algebraic reals, and traditional machine
word sizes such as Word8/Int8; 16; 32; and 64 symbolically.)

We plan to also add automatic support for SWordN/SIntN for arbitrary N,
once GHC gets proper support for type-level naturals.

Thanks to Brian Huffman for his contributions to this release. Bug
reports/comments are always welcome.

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell/attachments/20150122/fd73bae1/attachment.html>