Towards Automated Verification of Safety Architectures
Date Friday, January 11, 2002
Time 2-3pm
Speaker Carsten Schuermann
Affiliation Yale University
Abstract It is very unlikely that software will ever be proven totally correct, safe, and secure. For example, in order to trust that the execution of a binary is memory safe, we have to trust the correctness of the compiler implementation. But in general, we can neither expect any real compiler to be free of bugs nor can we expect to prove its implementation correct. On the other hand, when compiled code is augmented with safety proofs, the execution of the binary will be safe; in this case instead of trusting the compiler we must trust the safety architecture (e.g. proof-carrying code or typed assembly language) which is typically based on logics or type systems.

In my talk I will present a meta-logical framework and its implementation in the Twelf system. Twelf is a tool that supports the design of deductive systems in general and safety architectures in particular. In these domains its automated reasoning power far exceeds that of any other theorem prover. Specifically, Twelf has been successfully employed to derive various properties of logics and type systems directly relevant to safety architectures, such as the consistency of logics and the admissibility of new inference rules that shorten the size of safety proofs. Other results include automatic proofs of the Church-Rosser theorem, cut-elimination, and type preservation and progress of various operational semantics. Using one particular example, I will motivate the design of Twelf.
Location 545 Technology Square (aka "NE43")
Room 8th Floor Playroom
Bio Phd from CMU now assistant professor of Computer Science at Yale University.