<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">DEPARTMENT OF COMPUTER SCIENCE<div><br class="webkit-block-placeholder"></div><div>UNIVERSITY OF CHICAGO</div><div><br class="webkit-block-placeholder"></div><div>Date: Wednesday, April 9, 2008</div><div>Time: 2:30 p.m.</div><div>Place: Ryerson 251, 1100 E. 58th Street</div><div><br class="webkit-block-placeholder"></div><div>----------------------------------------------------------</div><div><br class="webkit-block-placeholder"></div><div>Speaker:<span class="Apple-tab-span" style="white-space: pre; "> </span>Christian Urban</div><div><br class="webkit-block-placeholder"></div><div>From:<span class="Apple-tab-span" style="white-space: pre; "> </span>TU Munich</div><div><br class="webkit-block-placeholder"></div><div>Web page:<span class="Apple-tab-span" style="white-space: pre; "> </span><font class="Apple-style-span" color="#144FAE"><span class="Apple-style-span" style="text-decoration: underline;"><a href="http://www4.in.tum.de/~urbanc/">http://www4.in.tum.de/~urbanc/</a></span></font></div><div><br class="webkit-block-placeholder"></div><div>Title: Verification of Programming Languages and Compilers</div><div><br class="webkit-block-placeholder"></div><div>Abstract: Recent years have seen much progress in developing
verified compilers. Such compilers guarantee that the compiled code behaves the
same as the source program where the behavior of both is prescribed by a specified semantics. Despite
this progress, however, the remaining problem is that the verification of a
compiler is still extremely hard. In my talk I will describe ideas for
simplifying such verifications. I will also describe techniques for the
verification of programming languages. The purpose of the latter is to
establish properties about compiled code that go beyond the behavioral
equivalence between source program and compiled code.</div><p class="MsoNormal" style="mso-pagination:none;mso-layout-grid-align:none;
text-autospace:none"><o:p></o:p></p>
<!--EndFragment-->
<p class="MsoNormal">---------------------------------------------------------</p><p class="MsoNormal">Host:<span class="Apple-tab-span" style="white-space: pre; "> </span>Dave MacQueen</p></body></html>