<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv=Content-Type content="text/html; charset=us-ascii">
<meta name=ProgId content=Word.Document>
<meta name=Generator content="Microsoft Word 11">
<meta name=Originator content="Microsoft Word 11">
<link rel=File-List href="cid:filelist.xml@01C78655.50271830">
<!--[if gte mso 9]><xml>
<o:OfficeDocumentSettings>
<o:DoNotRelyOnCSS/>
</o:OfficeDocumentSettings>
</xml><![endif]--><!--[if gte mso 9]><xml>
<w:WordDocument>
<w:SpellingState>Clean</w:SpellingState>
<w:GrammarState>Clean</w:GrammarState>
<w:DocumentKind>DocumentEmail</w:DocumentKind>
<w:EnvelopeVis/>
<w:ValidateAgainstSchemas/>
<w:SaveIfXMLInvalid>false</w:SaveIfXMLInvalid>
<w:IgnoreMixedContent>false</w:IgnoreMixedContent>
<w:AlwaysShowPlaceholderText>false</w:AlwaysShowPlaceholderText>
<w:Compatibility>
<w:BreakWrappedTables/>
<w:SnapToGridInCell/>
<w:WrapTextWithPunct/>
<w:UseAsianBreakRules/>
<w:UseWord2002TableStyleRules/>
<w:UseFELayout/>
</w:Compatibility>
<w:BrowserLevel>MicrosoftInternetExplorer4</w:BrowserLevel>
</w:WordDocument>
</xml><![endif]--><!--[if gte mso 9]><xml>
<w:LatentStyles DefLockedState="false" LatentStyleCount="156">
</w:LatentStyles>
</xml><![endif]-->
<style>
<!--
/* Font Definitions */
@font-face
{font-family:SimSun;
panose-1:2 1 6 0 3 1 1 1 1 1;
mso-font-alt:\5B8B\4F53;
mso-font-charset:134;
mso-generic-font-family:auto;
mso-font-pitch:variable;
mso-font-signature:3 135135232 16 0 262145 0;}
@font-face
{font-family:"\@SimSun";
panose-1:2 1 6 0 3 1 1 1 1 1;
mso-font-charset:134;
mso-generic-font-family:auto;
mso-font-pitch:variable;
mso-font-signature:3 135135232 16 0 262145 0;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{mso-style-parent:"";
margin:0pt;
margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:12.0pt;
font-family:"Times New Roman";
mso-fareast-font-family:SimSun;
mso-fareast-language:ZH-CN;}
a:link, span.MsoHyperlink
{color:blue;
text-decoration:underline;
text-underline:single;}
a:visited, span.MsoHyperlinkFollowed
{color:purple;
text-decoration:underline;
text-underline:single;}
p.MsoAutoSig, li.MsoAutoSig, div.MsoAutoSig
{margin:0pt;
margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:12.0pt;
font-family:"Times New Roman";
mso-fareast-font-family:"Times New Roman";}
span.EmailStyle17
{mso-style-type:personal-compose;
mso-style-noshow:yes;
mso-ansi-font-size:10.0pt;
mso-bidi-font-size:10.0pt;
font-family:Arial;
mso-ascii-font-family:Arial;
mso-hansi-font-family:Arial;
mso-bidi-font-family:Arial;
color:windowtext;}
span.GramE
{mso-style-name:"";
mso-gram-e:yes;}
@page Section1
{size:612.0pt 792.0pt;
margin:72.0pt 90.0pt 72.0pt 90.0pt;
mso-header-margin:36.0pt;
mso-footer-margin:36.0pt;
mso-paper-source:0;}
div.Section1
{page:Section1;}
-->
</style>
<!--[if gte mso 10]>
<style>
/* Style Definitions */
table.MsoNormalTable
{mso-style-name:"Table Normal";
mso-tstyle-rowband-size:0;
mso-tstyle-colband-size:0;
mso-style-noshow:yes;
mso-style-parent:"";
mso-padding-alt:0pt 5.4pt 0pt 5.4pt;
mso-para-margin:0pt;
mso-para-margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:10.0pt;
font-family:"Times New Roman";
mso-ansi-language:#0400;
mso-fareast-language:#0400;
mso-bidi-language:#0400;}
</style>
<![endif]--><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="2050" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang=EN-US link=blue vlink=purple style='tab-interval:36.0pt'>
<div class=Section1>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Guest Speaker<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Speaker: Xinyu Feng<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Speaker’s home page: <a
href="http://flint.cs.yale.edu/feng/">http://flint.cs.yale.edu/feng/</a><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Date: Tuesday, April 24, 2007<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Time: 10:00<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Location: TTI-C Conference room<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Title: An Open Framework for Building Certified System
Software<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><span style='mso-spacerun:yes'> </span><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Abstract:<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<span style='mso-spacerun:yes'>
</span>Constructing certified system software is an important step toward
building a reliable and secure computing platform for future critical
applications.<span style='mso-spacerun:yes'> </span>In addition to the
benefits from provably safe components, architectures of certified systems <span
class=GramE>may also be simplified</span> to achieve better efficiency.<span
style='mso-spacerun:yes'> </span>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<span class=GramE>. </span>As
a result, significant amount of kernel code of today's operating systems has to
<span class=GramE>be implemented</span> in unsafe languages, despite recent
progress on type-safe languages.<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<span style='mso-spacerun:yes'> </span>I will first present my
work on Hoare-style program logics for modular verification of low-level code.<span
style='mso-spacerun:yes'> </span>They <span class=GramE>have been applied</span>
to certify safety and partial correctness of memory management libraries,
thread libraries, garbage collectors, and concurrent programs.<span
style='mso-spacerun:yes'> </span>Then I will introduce an open and
extensible framework supporting interoperation between different verification
systems.<span style='mso-spacerun:yes'> </span>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.<o:p></o:p></span></font></p>
<p class=MsoAutoSig><font size=3 face="Times New Roman"><span style='font-size:
12.0pt;mso-no-proof:yes'><o:p> </o:p></span></font></p>
<p class=MsoNormal><span class=GramE><font size=3 face="Times New Roman"><span
style='font-size:12.0pt'>If you have any questions or would like to meet the
speaker,</span></font></span> please contact Ponda Barnes at <a
href="mailto:pondabarnes@tti-c.org">pondabarnes@tti-c.org</a><o:p></o:p></p>
<p class=MsoNormal><font size=3 face="Times New Roman"><span style='font-size:
12.0pt'>For future TTI-C talks and events please go to </span></font><font
size=2 face=Arial><span style='font-size:10.0pt;font-family:Arial'><a
href="http://ttic.uchicago.edu/cal/month.php"
title="http://ttic.uchicago.edu/cal/month.php">http://ttic.uchicago.edu/cal/month.php</a></span></font><o:p></o:p></p>
</div>
</body>
</html>