An article from Coverity writer: a static analysis tools

[Nicolas Boulay]

An interesting reading :

"The ideal: check millions of lines of code with little manual setup
and find the maximum number of serious true errors with the minimum
number of false reports. As much as possible, we avoided using
annotations or specifications to reduce manual labor."

"Our product did not verify the absence of errors but rather tried to
find as many of them as possible."

http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext