<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">We are very pleased to announce that a new version of LLBMC is available<br>for download at <a href="http://llbmc.org/">http://llbmc.org</a>.<br><br>LLBMC is a high-precision static analyzer based on LLVM implementing a<br>technique called "Bounded Model Checking". LLBMC can detect errors such as: <br>- Illegal memory accesses (e.g., buffer overflows) <br>- Integer overflows <br>- Division by zero <br>- Invalid bit shifts <br>- Double frees<br><br>The new version, 2013.1, offers several new features and improvements:<br><br>- LLBMC now performs lazy, on-demand loop unrolling, function inlining, and<br> encoding<br><br>- LLBMC can now take several bitcode files as input and it is no longer necessary<br> to use llvm-link in order to combine them into a single bitcode file<br><br>- Improved status information output<br><br>- LLBMC is now based on LLVM 3.3<br><br>- New version of STP (revision 1673)<br><br>- General stability and performance improvements</body></html>