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

[Hal Finkel]

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