[Colloquium] Talk by Frances Perry, Princeton University on February 25, 2008
caseyk
caseyk at cs.uchicago.edu
Mon Feb 18 14:31:46 CST 2008
DEPARTMENT OF COMPUTER SCIENCE
UNIVERSITY OF CHICAGO
Date: Monday, February 25, 2008
Time: 2:30 p.m.
Place: Ryerson 251, 1100 E. 58th Street
----------------------------------------------------------
Speaker: Frances Perry
From: Princeton University
Web page: http://www.cs.princeton.edu/~frances/
Title: Reasoning about Software in the Presence of Transient Faults
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.
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.
---------------------------------------------------------
Host: Dave MacQueen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20080218/9752c85f/attachment.html
More information about the Colloquium
mailing list