[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell
Subject:    [Haskell] [ANNOUNCE] New release of SBV
From:       Levent Erkok <erkokl () gmail ! com>
Date:       2015-01-23 6:31:38
Message-ID: CACOpX0choHPBLfkRXGn3zLTYNGwv_+Ez3nREb_edMz+PJ_Q-gQ () mail ! gmail ! com
[Download RAW message or body]

[Attachment #2 (multipart/alternative)]


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.

[Attachment #5 (text/html)]

<div dir="ltr">I&#39;m happy to announce a new release of SBV (v4.0); a library for \
seamlessly integrating SMT solvers with Haskell.<div><br></div><div>           <a \
href="https://hackage.haskell.org/package/sbv">https://hackage.haskell.org/package/sbv</a></div><div><br></div><div>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.)  </div><div><br></div><div>We plan to also \
add automatic support for SWordN/SIntN for arbitrary N, once GHC gets proper support \
for type-level naturals.</div><div><br></div><div>Thanks to Brian Huffman for his \
contributions to this release. Bug reports/comments are always \
welcome.</div><div><br></div><div>-Levent.</div></div>



_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell


[prev in list] [next in list] [prev in thread] [next in thread]