<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div><span class="Apple-style-span" style="background-color: transparent;">Perhaps some of you might be interested in this:</span></div><div>-- Carsten</div><div><br></div><div><span class="Apple-style-span" style="font-family: 'Courier New'; "><br></span></div><div><span class="Apple-style-span" style="font-family: 'Courier New'; ">##################################################################</span></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'"> *---------------------------------------------------*</font></div><div><font class="Apple-style-span" face="'Courier New'"> * LLBMC: The Low-Level Bounded Model Checker *</font></div><div><font class="Apple-style-span" face="'Courier New'"> * for C (and C++) programs is now available! *</font></div><div><font class="Apple-style-span" face="'Courier New'"> * Version 2012.1 *</font></div><div><font class="Apple-style-span" face="'Courier New'"> * <a href="http://llbmc.org/">http://llbmc.org</a> *</font></div><div><font class="Apple-style-span" face="'Courier New'"> *---------------------------------------------------*</font></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'">We are very pleased to announce that LLBMC, a bug-finding tool for</font></div><div><font class="Apple-style-span" face="'Courier New'">C (and, to some extent, C++) programs, is now available.</font></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'">LLBMC is a high-precision static analyzer implementing a technique</font></div><div><font class="Apple-style-span" face="'Courier New'">called "Bounded Model Checking". LLBMC is based on LLVM and can</font></div><div><font class="Apple-style-span" face="'Courier New'">detect errors such as:</font></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'">- Illegal memory accesses (e.g., buffer overflows)</font></div><div><font class="Apple-style-span" face="'Courier New'">- Integer overflows</font></div><div><font class="Apple-style-span" face="'Courier New'">- Division by zero</font></div><div><font class="Apple-style-span" face="'Courier New'">- Invalid bit shifts</font></div><div><font class="Apple-style-span" face="'Courier New'">- Double frees</font></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'">For more information and to download LLBMC see <a href="http://llbmc.org/">http://llbmc.org</a>.</font></div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div><div><font class="Apple-style-span" face="'Courier New'">##################################################################</font></div></div></div><div><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div><font class="Apple-style-span" face="'Courier New'"><br></font></div></div></div></div></body></html>