<html><head></head><body bgcolor="#FFFFFF"><div><div><span class="Apple-style-span" style="-webkit-tap-highlight-color: rgba(26, 26, 26, 0.296875); -webkit-composition-fill-color: rgba(175, 192, 227, 0.230469); -webkit-composition-frame-color: rgba(77, 128, 180, 0.230469); ">Am 07.02.2012 um 10:58 schrieb arrowdodger <<a href="mailto:6yearold@gmail.com">6yearold@gmail.com</a>>:</span><br></div><div><br></div><div></div><blockquote type="cite"><div>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?</div></blockquote><br><div>The goals of KLEE and LLBMC are quite similar (both are static analysis tools), the techniques to achieve this are different, though.</div><div><br></div><div>KLEE is based on a technique called "symbolic execution", LLBMC uses "bounded model checking".</div><div><br></div><div>In KLEE, individual program paths are encoded into a logical formula. For a check, such "symbolic paths" are enumerated and checked by a solver.</div><div><br></div><div>In contrast, LLBMC encodes all program paths (with restrictions on loop bounds and nested function calls) into a single formula and checks that.</div><div><br></div><div>Both approaches have their advantages and disadvantages: KLEE can suffer from an explosion in the number of program paths that have to be checked. In LLBMC, the single formula can become prohibitively large.</div><div>(Then manual partitioning techniques have to be used, e.g. checking individual functions.)</div><div><br></div><div>It's hard to say in advance which approach works better in which situation, but perhaps you may want to give LLBMC a try.</div><div><br></div></div><div>-- Carsten</div><div><span></span></div></body></html>