[Haskell-cafe] [Announce] New release of SBV is out

[Levent Erkok]

A new release of SBV is out (v4.1):

http://hackage.haskell.org/package/sbv-4.1

The main change in this release is the connection to Berkeley's ABC
<http://www.eecs.berkeley.edu/~alanmi/abc/> system, which is an industrial
strength synthesis and verification system. SBV can now generate proof
goals that are discharged by ABC, using state-of-the-art SAT based
techniques. ABC is especially extremely well-tuned for dealing with
problems in the bit-vector theory, and is heavily used in the hardware
industry as a backend verification tool.

Also included in this release is better support for IEEE-floats, and a
reworked implementation of the connection to the Boolector
<http://fmv.jku.at/boolector/> solver.

Thanks to Adam Foltzer of Galois for contributing the connection to ABC,
and Alan Mischenko from Berkeley to add the necessary infrastructure to ABC
to allow for this bridge to be built.

Full release notes:
https://github.com/LeventErkok/sbv/blob/master/CHANGES.md
SBV web page: http://leventerkok.github.io/sbv/

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150307/dd6e0fca/attachment.html>