[Colloquium] Guest Speaker Announcement

[Ponda Barnes]

Guest Speaker
 
Speaker: Xinyu Feng
Speaker's home page: http://flint.cs.yale.edu/feng/
 
Date: Tuesday, April 24, 2007
Time: 10:00
Location: TTI-C Conference room
 
 
Title: An Open Framework for Building Certified System Software
 
Abstract:
Certified software consists of a machine executable program plus a machine
checkable proof showing that the software is free of bugs with respect to a
particular specification.  Constructing certified system software is an
important step toward building a reliable and secure computing platform for
future critical applications.  In addition to the benefits from provably
safe components, architectures of certified systems may also be simplified
to achieve better efficiency.  However, because system software consists of
program modules that use many different computation features and span
different abstraction levels, it is difficult to design a single type system
or program logic to certify the whole system. As a result, significant
amount of kernel code of today's operating systems has to be implemented in
unsafe languages, despite recent progress on type-safe languages.
 
In this talk, I will present a new methodology for constructing certified
system software: we develop different verification systems to certify
program modules at different abstraction levels, and use a new open
framework to link these certified modules to build a fully certified system.
I will first present my work on Hoare-style program logics for modular
verification of low-level code.  They have been applied to certify safety
and partial correctness of memory management libraries, thread libraries,
garbage collectors, and concurrent programs.  Then I will introduce an open
and extensible framework supporting interoperation between different
verification systems.  In this framework, we have successfully linked
certified concurrent code with certified thread libraries, and typed
assembly language code with certified garbage collectors and memory
management libraries, both of which were previously open research problems.
 
If you have any questions or would like to meet the speaker, please contact
Ponda Barnes at pondabarnes at tti-c.org
For future TTI-C talks and events please go to
http://ttic.uchicago.edu/cal/month.php
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20070424/73bc4567/attachment.html