Harvard University
Computer Science Colloquium Series
33 Oxford St., Cambridge, MA 02138
Colloquium
Automatic termination proofs for software
Byron Cook
Microsoft
http://research.microsoft.com/~bycook
Thursday, March 1, 2007
4:00PM
Maxwell Dworkin G125
(Ice Cream at 3:30PM - Maxwell Dworkin 2nd Floor Lounge Area)
Abstract
I will describe recent advances in the area of automatic program
termination analysis. I will also discuss TERMINATOR, the Microsoft
tool which implements these recent advances. We've recently used
TERMINATOR to prove that Windows device driver dispatch routines always
return control back to their caller. TERMINATOR has also found a number
of critical termination bugs in device drivers.
Host: Professor Norman Ramsey
_______________________________________________
Colloquium mailing list
Colloquium(a)deas.harvard.edu
https://lists.deas.harvard.edu/mailman/listinfo/colloquium
_______________________________________________
iic-seminars mailing list
iic-seminars(a)calists.harvard.edu
http://calists.harvard.edu/mailman/listinfo/iic-seminars