[Haskell-cafe] [Announcement] New release of SBV: SMT Based Verification, v3.0

[Levent Erkok]

Home page: http://leventerkok.github.io/sbv/
ChangeLog: http://github.com/LeventErkok/sbv/blob/master/CHANGES.md

I'm happy to announce a new release of SBV, v3.0.

The most important addition is support for reasoning about IEEE-74 floating
point numbers, i.e., programs using the Float and Double types. See the
change-log for full details.

Reasoning with floating-point is a tricky task, and SMT solvers are slowly
starting to provide support for true machine arithmetic as prescribed by
the IEEE-754 standard. In particular, the semantics of NaN and Infinity are
both properly captured, along with proper rounding. Also supported is
fused-multiply-add, and square-root functions at the logic level.

Currently, only Z3 (the developer version release) has official support for
this logic, and the implementation in SBV builds on top of Z3's
implementation. It's likely that both Z3's and SBV might have some rough
edges, so any bug reports are most welcome.

There's also a new example file demonstrating the floating-point
arithmetic: Formally establishing that floating point addition is not
associative (finding a concrete counter-example),  multiplicative inverses
do not necessarily exist, etc. See:
http://hackage.haskell.org/package/sbv-3.0/docs/Data-SBV-Examples-Misc-Floating.html

Happy theorem proving!

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140216/9ed97ef5/attachment.html>