<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: Monday, February 25, 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>Frances Perry</div><div><br class="webkit-block-placeholder"></div><div>From:<span class="Apple-tab-span" style="white-space:pre"> </span>Princeton University</div><div><br class="webkit-block-placeholder"></div><div>Web page:<span class="Apple-tab-span" style="white-space:pre"> </span><a href="http://www.cs.princeton.edu/~frances/">http://www.cs.princeton.edu/~frances/</a></div><div><br class="webkit-block-placeholder"></div><div>Title: Reasoning about Software in the Presence of Transient Faults</div><div><br class="webkit-block-placeholder"></div><div>Abstract: A transient hardware fault occurs when an energetic
particle strikes a transistor, causing it to change state. Although transient
faults do not permanently damage the hardware, they may corrupt computations by
altering stored values and signal transfers. Existing solutions can detect
transient faults by duplicating computations and comparing the results, however
these solutions lack any formal reasoning about their behavior. </div><p class="MsoNormal" style="mso-pagination:none;mso-layout-grid-align:none;
text-autospace:none"><o:p></o:p></p><p class="MsoNormal" style="mso-pagination:none;mso-layout-grid-align:none;
text-autospace:none">In this talk, I will show how to use low-level type
systems to cleanly express invariants about redundant computations and to
formally reason about code behavior, even when execution may be affected by
transient faults. In particular, I will present a typed assembly language named
TAL_FT and use it to prove that well-typed programs will always detect any
single fault before the fault causes a change in the program output.<span style="font-size:11.0pt;font-family:Helvetica"><o:p></o:p></span></p><p class="MsoNormal" style="mso-pagination:none;mso-layout-grid-align:none;
text-autospace:none">---------------------------------------------------------</p><p class="MsoNormal" style="mso-pagination:none;mso-layout-grid-align:none;
text-autospace:none">Host:<span class="Apple-tab-span" style="white-space:pre"> </span>Dave MacQueen</p>
<!--EndFragment-->
</body></html>