LLBMC (Low-Level Bounded Model Checker) - Analyzes C/C++ code to detect bugs (baldur.iti.uka.de)