|Towards Automated Verification of Safety Architectures|
|Date||Friday, January 11, 2002|
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.|