Byron Cook

Dr. Byron Cook is researcher at Microsoft's laboratory at Cambridge University. Dr. Cook is known for his research on automating the search for program termination proofs (TERMINATOR), automatic tools for proving properties of programs that make non-trivial use of the heap (SLAyer), and automatic tools for proving safety properties of software systems (SLAM).

Dr. Cook is one of the developers behind the Windows product Static Driver Verifier, which attempts to automatically prove the correctness of Windows OS device drivers with respect to a fixed set of safety properties. For more information, see http://research.microsoft.com/~bycook.

Presentation: "Halting problem, no problem!"

Track: Five Things I Wish I Learned In College

Time: Friday 09:30 - 10:30

Location: Cornell

Abstract:

Recent advances mean that a new post-halting-problem era is coming in which we will have tools that can automatically prove termination, tools that can automatically tell us conditions in which code will terminate, and even runtimes that ensure that code won't diverge while it's running.

This talk will show off some of these tools and describe how they work.

Password protected Download slides