Coverity, the company formed by the people behind the Stanford MC Checker, has started posting regular reports from their analysis tools on prominent open-source projects at scan.coverity.com.
I found out about this through an email from the Coverity CTO on the GCC mailing list, and it seems to have been received with some moderate enthusiasm. I think it’s a good idea, but as usual the specter of false positives makes the developers itchy, especially when they’re publishing bug counts…
Dawson Engler, the professor at Stanford who was behind all this bug-finding work (and co-founded Coverity) gave a talk recently here at CSE, about newer approaches to finding bugs that uses execution on symbolic inputs - meaning that you mark some inputs to a program as symbolic, and somewhere there’s a theorem prover that goes to work finding out if any value of those inputs can cause an error or a crash - then you can run the original code on the input to verify the problem. A nice consequence here is that the generated ‘bad’ input is then guaranteed to actually be bad, since you can test it and force the error.
There’s a paper about that from Engler’s group here, and apparently this PLDI 2005 paper from Bell Labs is very similar.
Here’s Prof. Engler’s slides from talks about the new work on bug finding and an entertaining talk about commercializing the MC Checker.
8:00 pm March 13, 2006
under programming, research
No Comments yet. Add one?
