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

Carsten Sinz carsten.sinz at kit.edu
Mon Feb 6 16:58:58 PST 2012


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>


More information about the llvm-dev mailing list