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, the correctness of the compiler implementation must be trusted. But in general, no one can expect that 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 this talk Carsten Schuermann 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. Schuermann 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.