[LLVMdev] Announcement: LLBMC, the Low-Level Bounded Model Checker

[arrowdodger]

On Tue, Feb 7, 2012 at 4:58 AM, Carsten Sinz <carsten.sinz at kit.edu> wrote:

> Perhaps some of you might be interested in this:
> -- Carsten
>
>
> ##################################################################
>
>     *---------------------------------------------------*
>     *    LLBMC: The Low-Level Bounded Model Checker     *
>     *    for C (and C++) programs is now available!     *
>     *                   Version 2012.1                  *
>     *                  http://llbmc.org                 *
>     *---------------------------------------------------*
>
> We are very pleased to announce that LLBMC, a bug-finding tool for
> C (and, to some extent, C++) programs, is now available.
>
> LLBMC is a high-precision static analyzer implementing a technique
> called "Bounded Model Checking". LLBMC is based on LLVM and can
> detect errors such as:
>
> - Illegal memory accesses (e.g., buffer overflows)
> - Integer overflows
> - Division by zero
> - Invalid bit shifts
> - Double frees
>
> For more information and to download LLBMC see http://llbmc.org.
>
> ##################################################################
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
>
Maybe it's somewhat dumb question - is it somehow related with KLEE?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20120207/482da8f5/attachment.html>