When & Where: 12:30pm, Friday, September 19, 2008, Room 200 AKW
Abstract:
The certification of programs using the CAP framework has resulted in many powerful certification systems. In particular, the non-CPS style version of the framework that uses a control stack, SCAP, follows traditional Hoare-logic style certification, and has been very promising. However, the process of certification has been very tedious due to the low-level nature of this framework. This SPAM talk will be a presentation and a discussion of pros and cons of a newly-developed method of certification whose core is quite similar to the SCAP framework. The main idea of this framework is that programs and machines are further abstracted into a common meta-level at which the certification is performed. This allows different machines and programs to be certified using a common system, providing a way to precisely define abstraction.