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

[Carsten Sinz]

Am 07.02.2012 um 10:58 schrieb arrowdodger <6yearold at gmail.com>:

> 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?

The goals of KLEE and LLBMC are quite similar (both are static analysis tools), the techniques to achieve this are different, though.

KLEE is based on a technique called "symbolic execution", LLBMC uses "bounded model checking".

In KLEE, individual program paths are encoded into a logical formula. For a check, such "symbolic paths" are enumerated and checked by a solver.

In contrast, LLBMC encodes all program paths (with restrictions on loop bounds and nested function calls) into a single formula and checks that.

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.
(Then manual partitioning techniques have to be used, e.g. checking individual functions.)

It's hard to say in advance which approach works better in which situation, but perhaps you may want to give LLBMC a try.

-- Carsten
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20120208/fef39227/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5811 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20120208/fef39227/attachment.bin>