Frama-C to prove formal properties for critical software.

I just came across a project, which has been around for a couple of years, that looks like it could be very useful: Frama-C. Frama-C stands for Framework for Modular Analysis of C programs.

Frama-C is intended to be an extensible static analyzer, that can prove formal properties for critical software. Frama-C does static analysis, dead code removal, security checks, and other functions depending on which plug-ins are used.

Armand, one of the project participants, is working on implementing the MISRA-C 2004 rules for the static analyzer.

Trying out Frama-C: analyzing a simple C program.