C++ static and runtime verifiers, security compliance, model checking/metacomplication, and program restructuring tools

The following is a list of C++ static and runtime verifiers, security compliance, model checking/metacomplication, and program restructuring tools as compiled by David Bremner.

Static Verifiers:
Spark is a high integrity dialect of Ada that's intended for use in safety/mission critical applications. There are a number of interesting case studies on their website. High Integrity Software: The SPARK Approach to Safety and Security by John Barnes is a book about it (It comes with a demo copy of the Spark tools. I haven't read it yet).

The MISRA Guidelines for using C in safety-critical applications. They recommend doing so only as a last resort.

Oakwood Computing is Les Hatton's company. They sell a static analyzer intended for C in safety-critical systems. Professor Hatton also wrote Safer C, an excellent book on the same topic (I've read the first edition).

Programming Research sells analyzers for C, C++, and Java.

Polyspace sells a verifier that uses abstract interpretation. It supports C, C++, and Ada. Their product is written in Standard ML and compiled with mlton.

Runtime Verifiers:
Valgrind is an excellent system for detecting cache misses, memory leaks, threading errors, etc. It uses a JIT compiler to trace every instruction. For x86/Linux.

Security Vulnerability Scanners:
BOON is a static checker for buffer overflows

Secure Programming Lint

Flawfinder

ITS4

RATS

Model checking and metacompliation:
CCured rewrites C programs to use GC and bounds-checking, albeit with a performance hit.

CQual is a tool for adding type qualifiers to C

MOPS is a model checker for C

Stanford's Meta-level compilation project, no tools are freely available.

Coverity was founded by some of the Stanford researchers. They provide customized model checking for individual codebases.

Smatch is a clone of the Metacomp tools based on the papers published about it. It's been used by the Linux kernel and the WINE project.

Program Restructuring:
Semantic Designs sells a variey of software engineering tools. To quote from their website: "A set of tools for carrying out custom re-engineering of medium and large scale software systems (documentation extraction, analysis, porting, translation, modification, interface changes, or other massive regular change) and/or domain-specific program generation."

The Stratego transformation language.

Open C++. "OpenC++ is a C++ frontend library (lexer+parser+DOM/MOP) and source-to-source translator. OpenC++ enables development of C++ language tools, extensions, domain specific compiler optimizations and runtime metaobject protocols."

CodeBoost is a C++ transformation framework written by some Norwegian researchers. It uses Stratego and Open C++.

Recommended Reading:
Why Do Computers Stop and What Can Be Done About It?

Uses and Abuses of Statement Coverage

Plan Into Practice Software Testing at Tandem Computers