Colloquium Details
Towards Automated Verification of Safety Architectures
| Author: | Carsten Schuermann Department of Computer Science, Carnegie Mellon University |
|---|---|
| Date: | March 28, 2000 |
| Time: | 16:00 |
| Location: | 220 Deschutes |
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 Twelf, a tool that supports the design and verification of safety architectures. More generally, Twelf is designed to reason about logical systems which are prevalent in areas such as a programming languages and type systems. During my talk I will pay special attention to the design of the automated deduction component of Twelf. Its reasoning power far exceeds that of any other theorem prover in these specialized domains.