Flawfinder searches through source code looking for potential security flaws. It will provide a list of potential security flaws, sorted by risk, with the most potentially dangerous flaws shown first. This risk level depends not only on the function, but on the values of the parameters of the function. Flawfinder ignores text inside comments and strings.
Fenris is a multipurpose tracer, debugger, and code analysis tool that detects and documents high-level language constructions, can recover symbols, graph program execution flow, detect internal functions, recover symbol tables, and deal with anti-debugging protection. It features a command-line interface as well as a SoftICE-alike GUI and Web frontend.
ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.
zzuf is a transparent application input fuzzer. Its purpose is to find bugs in applications by corrupting their user-contributed data, which frequently comes from untrusted sources on the Internet. It works by intercepting file and network operations and changing random bits in the program's input. zzuf's behavior is deterministic, making it easier to reproduce bugs.
Oink is a collaboration of backends for the Elsa C and C++ frontend. It aims to be industrial-strength for immediate utility in finding bugs, extensible for ease in adding backends, and composable for ease in combining existing ones. It computes expression-level and type-level data flow, and statement-level intra-procedural control flow (by delegating to Elsa). It's easy to get started by using the two demo backends that print graphs of these flows. It also comes with a client of the data flow analysis that does type qualifier inference: Cqual++, a C/C++ frontend for Cqual. Whole-program analyses may be attempted using the linker imitator.