Wednesday, June 22, 2005
Sorry for the delay on this report. My body shut down last night and I just couldn't get to it.
Okay, following Paul Dietz's talk about the Common Lisp test suite, I attended Arthur Nunes-Harwitt's talk titled Advice about Debugger Construction. This was an interesting talk about how Lisp debuggers should be implemented, following a basic principle of least astonishment for a user.
The next talk was James McDonald's Correctness-by-Construction is in your future. James's basic thesis is that the size of software systems is rapidly increasing, past the point where we can actually verify their correctness using standard testing techniques. Rather than constructing software by writing standard algorithms in the future, James argues for a world in which specifications are translated into a formal language, from which "real" code is synthesized. James cited a bake-off done by the NSA where this method was substantially more effective at reducing defects than the more traditional UML-based design methodology.
The highlight of the day was J. Strother Moore's A Mechanized Program Verifier. Moore is the Moore in Boyer-Moore string matching and various other automated proving algorithms. That alone was worth the price of admission. Moore is, frankly, just a good speaker. His talk was very well put together. McDonald's talk was a great setup for Moore's and they both echoed similar themes. Moore, along with Boyer previously, has been working on automated theorem proving for quite some time. Using a subset of Common Lisp, called Applicative Common Lisp, Moore and his team have developed a system that can prove theorems, provided with a series of lemmas. Moore quickly made the case that this sort of mechanized proving has great commercial utility. Moore described Intel's debacle with the Pentium FDIV bug. This mistake caused Intel to take a ~$470M charge on their financials. AMD was about to introduce the K5 just after that and hired Moore's team to verify the floating point unit. This technique has been repeatedly used since that time at AMD to verify the floating point portions of their chip.
Moore also described work that has gone on with Sun to verify the behavior of the Java virtual machine. Moore's team has constructed a 700-page description of the JVM and has used that to verify various properties of the Java byte-code verifier. Additional applications included verification of various floating point processors (Power 4, K5, Athlon, and Opteron), verification of DSP microcode (Motorola), and verification of the security policy of Rockwell Collins's AAMP 7 microprocessor.
What made Moore's talk so fun was that he showed some simple live demos of the system. It was very interesting to see things run and theorems being proved. When Moore ended his talk, he got the closest thing to a standing ovation that you could receive.
Links to this post: