Hacker News Reader

Paraphrasing Dijkstra: “Using static code analysis shows the presence, not the absence of bugs.”

See: (1) “Finding Heartbleed with CodeSonar”, (2) “Why Do Software Assurance Tools Have Problems Finding Bugs Like Heartbleed?”

[1] http://blogs.grammatech.com/finding-heartbleed-with-codesona...

[2] https://www.swampinabox.org/doc/SWAMP-WP003-Heartbleed.pdf

View on HN

I think that's a misapplication of the quote. Testing just checks an algorithm on specific inputs. The proofs check it for all inputs. Some static analyzers are designed to show absence of bugs of specific type for all inputs. They're more like proof.

Astree Analyzer and TrustinSoft Analyzer are examples that claim to prove absence of errors with sound analysis.

Reply on news.ycombinator.com