New version (2013.1) of LLBMC available

[LLBMC]

We are very pleased to announce that a new version of LLBMC is available

for download at http://llbmc.org!

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

  encoding

- 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