New version (2013.1) of LLBMC available

Skip to first unread message


Jun 20, 2013, 12:32:16 PM6/20/13
We are very pleased to announce that a new version of LLBMC is available
for download at!

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

The new version, 2013.1, offers several new features and improvements:

- LLBMC now performs lazy, on-demand loop unrolling, function inlining, and

- LLBMC can now take several bitcode files as input and it is no longer necessary
  to use llvm-link in order to combine them into a single bitcode file

- Improved status information output

- LLBMC is now based on LLVM 3.3

- New version of STP (revision 1673)

- General stability and performance improvements
Reply all
Reply to author
0 new messages