When & Where: 12:30pm, Wednesday, Oct 30, 2002, Room 400 AKW
Abstract:
Programs are notoriously unreliable and program proofs often impossible. A possible alternative is provided by Proof-Carrying Code (PCC), where a program is provided along with a certificate that makes correctness at least partially provable. There exist now a couple of approaches to PCC that lead to different PCC architectures. Most of them talk about applying their specific framework to arbitrary safety properties, but up to now they deal only with memory safety.
In this talk, we want to present a project idea on how to handle different safety properties for PCC in an abstract and modular way. The idea is to formalize the PCC framework and thus to provide a machine checked verification of all components. The model will be generic with respect to the machine and the syntax and semantics of the programming language and safety logic. We intended to instantiate the model with safety logics for time and space constraints and arithmetic.