Automatic termination proofs for software

Add to your list(s) Download to your calendar using vCal

• Byron Cook, Microsoft Research
• Wednesday 15 November 2006, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Timothy G. Griffin.

I will describe recent advances in the area of automatic program termination analysis. In particular, I will describe the development of several automatic tools, called TERMINATOR and MUTANT , which implement new termination analysis algorithms. These tools have been used to prove that Windows device driver dispatch routines always return control back to their caller. The tools have also found a number of critical termination bugs in device drivers.

Bio: Dr. Byron Cook is a researcher at Microsoft Research, Cambridge. His research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Before coming to Cambridge Byron co-developed the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. Before joining Microsoft, Byron worked at Prover Technology. Byron’s PhD is from OGI . For more information about Byron, see http://research.microsoft.com/~bycook.

This talk is part of the Computer Laboratory Wednesday Seminars series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Wednesday Seminars
• Computer Laboratory talks
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.