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

[Carsten Sinz]

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>