Static verification is the set of processes that analyzes code to ensure defined coding practices are being followed. This includes, but is not limited to, checking to ensure coding conventions are being followed and banned functions aren't being used. Additionally, static verification includes metrics (examples of metrics could be lines of code, bugs per line(s) of code or lines of code checked for vulnerabilities). Finally, static verification also includes formal verification, which is the attempt to use formal mathematical proofs to demonstrate that particular code adheres to specifications; this is particularly useful in terms of cryptography and algorithms, but has very broad applications as well.
Source code analysis is great; it catches all sorts of issues especially around assorted overflows and underflows as well as use of banned functions. Binary analysis is very complimentary to source code analysis as it is really good at catching more complex buffer overflow issues, but also at finding application logic issues that would otherwise might only be caught by a very experienced manual code review team. In either case, these automated tools can cover far more code then a human code reviewer, freeing them up to focus on more complex architectural issues.
For more information:
This was first published in August 2009