Dawson Engler, who previously developed a tool called Metal to detect hundreds of real errors in real code (e.g. the Linux kernel), has now co-authored a paper on Using Redundancies to Find Errors. The idea is that redundant code is often not merely inefficient, but a sign that a programmer is “confused” about what the code does, and the results seem to bear that out; code containing flagged redundancies was 45-100% more likely to contain serious errors than other code. Some of the examples are really interesting.

I also noticed that Engler has collaborated with David Dill, one of the authors of Murphi, on a paper entitled CMC: A pragmatic approach to model checking real code. I’ll have to check that one out soon.