On Tue, Feb 7, 2012 at 4:58 AM, Carsten Sinz <span dir="ltr"><<a href="mailto:carsten.sinz@kit.edu">carsten.sinz@kit.edu</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div style="word-wrap:break-word"><div style="word-wrap:break-word"><div><div><span style="background-color:transparent">Perhaps some of you might be interested in this:</span></div><div>-- Carsten</div><div><br></div><div>

<span style="font-family:'Courier New'"><br></span></div><div><span style="font-family:'Courier New'">##################################################################</span></div><div><font face="'Courier New'"><br>

</font></div><div><font face="'Courier New'">    *---------------------------------------------------*</font></div><div><font face="'Courier New'">    *    LLBMC: The Low-Level Bounded Model Checker     *</font></div>

<div><font face="'Courier New'">    *    for C (and C++) programs is now available!     *</font></div><div><font face="'Courier New'">    *                   Version 2012.1                  *</font></div>
<div>
<font face="'Courier New'">    *                  <a href="http://llbmc.org/" target="_blank">http://llbmc.org</a>                 *</font></div><div><font face="'Courier New'">    *---------------------------------------------------*</font></div>

<div><font face="'Courier New'"><br></font></div><div><font face="'Courier New'">We are very pleased to announce that LLBMC, a bug-finding tool for</font></div><div><font face="'Courier New'">C (and, to some extent, C++) programs, is now available.</font></div>

<div><font face="'Courier New'"><br></font></div><div><font face="'Courier New'">LLBMC is a high-precision static analyzer implementing a technique</font></div><div><font face="'Courier New'">called "Bounded Model Checking". LLBMC is based on LLVM and can</font></div>

<div><font face="'Courier New'">detect errors such as:</font></div><div><font face="'Courier New'"><br></font></div><div><font face="'Courier New'">- Illegal memory accesses (e.g., buffer overflows)</font></div>

<div><font face="'Courier New'">- Integer overflows</font></div><div><font face="'Courier New'">- Division by zero</font></div><div><font face="'Courier New'">- Invalid bit shifts</font></div><div>

<font face="'Courier New'">- Double frees</font></div><div><font face="'Courier New'"><br></font></div><div><font face="'Courier New'">For more information and to download LLBMC see <a href="http://llbmc.org/" target="_blank">http://llbmc.org</a>.</font></div>

<div><font face="'Courier New'"><br></font></div><div><font face="'Courier New'">##################################################################</font></div></div></div><div><div style="word-wrap:break-word">

<div><div><font face="'Courier New'"><br></font></div></div></div></div></div><br>_______________________________________________<br>
LLVM Developers mailing list<br>
<a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
<br></blockquote></div><br>Maybe it's somewhat dumb question - is it somehow related with KLEE?<br>