Low Level Bounded Model Checker

[Ulrik Mikaelsson]

I just saw this on Google Tech talks, and thought others on the list
might enjoy it; http://www.youtube.com/watch?v=vajMUlyXw_U

It's about LLBMC, an automated program-prover targeting automated
proofing for functional-style programs. The idea is to go a step
beyond specific test-cases, and prove function correctness for all
possible input values. The method is to compile the source (currently
only C supported, with C++ on the way) using Clang to LLVM-IR, and
perform the analysis on the LLVM-IR-level.

Now, in D I think most of the meta-information framework required is
already present in the language (for C, they've added some
meta-keywords), especially DBC-programming with in and out-validators.
A LLBMC-like version for D should in theory be able to use only the
existing in/out/invariant/assert-clauses. However, it would be a VERY
useful tool able to auto-validate all functional code against it's
contract.

http://baldur.iti.uka.de/llbmc/