Announcement: LLBMC, the Low-Level Bounded Model Checker

Perhaps some of you might be interested in this:
– Carsten

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

-Hal

Maybe it’s somewhat dumb question - is it somehow related with KLEE?

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

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