llvm dev - Feb 2012 - [LLVMdev] Announcement: LLBMC, the Low-Level Bounded Model Checker

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.

##################################################################

-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20120207/b2ada8f5/attachment.html>

This looks very interesting. Do you plan to make the source code
publicly available?

 -Hal

On Tue, 2012-02-07 at 01:58 +0100, Carsten Sinz 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
-- 
Hal Finkel
Postdoctoral Appointee
Leadership Computing Facility
Argonne National Laboratory

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>

For our first release we have decided not to make the source code publicly
available. Future releases may come under a different license, though, and
include the source code.

-- Carsten

Am 07.02.2012 um 05:38 schrieb Hal Finkel <hfinkel at anl.gov>:
> This looks very interesting. Do you plan to make the source code
> publicly available?
> 
> -Hal
> 
> On Tue, 2012-02-07 at 01:58 +0100, Carsten Sinz 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
> 
> -- 
> Hal Finkel
> Postdoctoral Appointee
> Leadership Computing Facility
> Argonne National Laboratory
> 
-------------- 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/20120207/0684f017/attachment.bin>

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>