When & Where: 12:00pm, Friday, September 17, 2010, Room 307 AKW
Abstract:
Several recent projects have involved machine-checked proofs of correctness for programs in assembly language or other not-much-higher abstraction levels. "Machine-checked proofs" can mean many things. Projects that rely on automated theorem-provers typically lead to the least programmer effort per unit of assurance. However, automated tools tend not to do well with higher-order goals, such as reasoning about first-class code pointers or proofs of type system soundness. The more the automated prover can do, the more reason there is to worry that prover has a critical soundness bug. In contrast, other recent work has used interactive proof assistants, such that program verifications may be trusted without believing in the correctness of much more than a small, generic proof checker and some basic formalization of language semantics. The programmer overhead of these systems has been shown to be rather higher than with automated tools, sometimes at the level of hundreds of lines of proof per program instruction.
The Bedrock framework is a new library for Coq that combines some of the characteristic advantages of the two prior approaches. Higher-order reasoning is readily supported, via Coq's usual mechanisms; and the trusted code base for a program verification depends only on the Coq core and simple operational semantics for machine languages. At the same time, structured programming is supported, in the style of traditional reasoning with axiomatic semantics; and proofs can be automated about as effectively as in recent (non-foundational) work in that style. We have verified a number of example programs so far, including one (list append in CPS with explicit closures) that requires orders of magnitude less proof code than in past work which posed it as a challenge problem.
Biography:
Adam Chlipala is currently a postdoc in computer science at Harvard University. His research centers on improving the whole software stack, using tools for mechanized reasoning about programs, including interactive theorem-proving and type systems. He finished his PhD at Berkeley in 2007, with a thesis on verifying compilers and program analysis tools in the Coq computer proof assistant. At Harvard, he has worked on compiler verification and on frameworks for mostly-automated verification of higher-order, imperative programs, via separation logic. He is also working on the domain-specific language Ur/Web, which applies ideas from dependent types and theorem-proving to give static guarantees about popular web application idioms.