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

[Niklas Hambüchen]

Hi,

this is pretty darn cool.

Short technical question: Why functions on SInteger so much faster to
check than functions on SWord32? Is it because they don't overflow?

Also I think RebindableSyntax would be really useful for this.
I have seen your counter arguments in
https://github.com/LeventErkok/sbv/issues/79, but RebindableSyntax would
make checking many functions really easy. I think your idea with making
it a separate module is the right way, e.g. Data.SBV.RebindableSyntax.

Niklas

On 16/02/14 23:50, Levent Erkok wrote:
> 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.
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>