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.