<div dir="ltr"><div><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px">A new release of SBV is out (v4.1):</span><br></div><div><br style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px"><a rel="nofollow" href="http://hackage.haskell.org/package/sbv-4.1" dir="ltr" style="color:rgb(66,127,237);text-decoration:none;font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px" target="_blank">http://hackage.haskell.org/package/sbv-4.1</a><br style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px"><br>The main change in this release is the connection to Berkeley's <a href="http://www.eecs.berkeley.edu/~alanmi/abc/">ABC</a> system<span style="font-size:13px;color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;line-height:18.2000007629395px">, </span><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px">which is an industrial strength synthesis and verification system. SBV can now generate proof goals that are discharged by ABC, using state-of-the-art SAT based techniques. ABC is especially extremely well-tuned for dealing with problems in the bit-vector theory, and is heavily used in the hardware industry as a backend verification tool.</span></div><div><br></div><div>Also included in this release is better support for IEEE-floats, and a reworked implementation of the connection to the <a href="http://fmv.jku.at/boolector/">Boolector</a> solver.</div><div><br></div><div><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px">Thanks to Adam Foltzer of Galois for contributing the connection to ABC, and </span><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px">Alan Mischenko from Berkeley to add the necessary infrastructure to ABC to allow for this bridge to be built.</span><br></div><div><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px"><br></span></div><div><span style="color:rgb(64,64,64);font-family:Roboto,arial,sans-serif;font-size:13px;line-height:18.2000007629395px">Full release notes: </span><font color="#404040" face="Roboto, arial, sans-serif"><span style="line-height:18.2000007629395px"><a href="https://github.com/LeventErkok/sbv/blob/master/CHANGES.md">https://github.com/LeventErkok/sbv/blob/master/CHANGES.md</a></span></font></div><div><font color="#404040" face="Roboto, arial, sans-serif"><span style="line-height:18.2000007629395px">SBV web page: <a href="http://leventerkok.github.io/sbv/">http://leventerkok.github.io/sbv/</a></span></font></div><div><font color="#404040" face="Roboto, arial, sans-serif"><span style="line-height:18.2000007629395px"><br></span></font></div><div><font color="#404040" face="Roboto, arial, sans-serif"><span style="line-height:18.2000007629395px">-Levent.</span></font></div></div>