<div dir="ltr">I'm happy to announce a new release (v5.4) of SBV: SMT Based Verification. See: <a href="http://hackage.haskell.org/package/sbv" target="_blank">http://hackage.haskell.org/package/sbv</a><div><br></div><div>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 href="http://hackage.haskell.org/package/sbv-5.4/docs/Data-SBV.html#g:39" target="_blank">http://hackage.haskell.org/package/sbv-5.4/docs/Data-SBV.html#g:39</a></div><div><br></div><div>A slightly larger example checks for lack-of-division-by-0 in a simple program: <a href="http://hackage.haskell.org/package/sbv-5.4/docs/Data-SBV-Examples-Misc-NoDiv0.html" target="_blank">http://hackage.haskell.org/package/sbv-5.4/docs/Data-SBV-Examples-Misc-NoDiv0.html</a></div><div><br></div><div>Further documentation on SBV is available at: <a href="http://leventerkok.github.io/sbv/" target="_blank">http://leventerkok.github.io/sbv/</a></div><div><br></div><div>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..</div><div><br></div><div>Happy proving.</div><div><br></div><div>-Levent.</div><div><br></div><div>PS. Thanks to Brett Letner for suggesting this functionality.</div></div>