[Haskell-cafe] [ANN] SBV 5.4 is out

Levent Erkok erkokl at gmail.com
Tue Nov 10 03:03:34 UTC 2015

I'm happy to announce a new release (v5.4) of SBV: SMT Based Verification.
See: http://hackage.haskell.org/package/sbv

New in this release is the 'sAssert' function, which allows
boolean-assertions to be sprinkled in symbolic code, which can then be
statically discharged (or shown violating assignments for) using the 'safe'
function. See:

A slightly larger example checks for lack-of-division-by-0 in a simple

Further documentation on SBV is available at:

Calls to sAssert calls are also preserved in the SBV->C compilation path.
This feature is rather experimental and , and I'd love to hear if you give
it a try and see any gotchas..

Happy proving.


PS. Thanks to Brett Letner for suggesting this functionality.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151109/55bebed1/attachment.html>

More information about the Haskell-Cafe mailing list