Byron Cook: Terminator - Proving Good Things Will Eventually Happen

Download this episode

Download Video


Here's another installment from MSR Cambridge (much more to come). This time, I was lucky enough to get some time with Byron Cook, a researcher in MSR's Programming Principles and Tools group focusing on static analysis of system code to hunt for algorithms and code fragments that will most likely induce a system state lovingly referred to by all as a Hang. You know, when nothing seems to work anymore, you can't use your mouse or keyboard, windows are frozen in time and you resort to a hard reboot. Well, what is a hang, exactly? How is a hang directly related to events? Did you know that a typical hang is event-related (never ending event response) caused by kernel mode code (drivers mostly) that never, well, terminates?

Byron and team have written a very interesting tool that analyzes code, tests it against proofs of correctness (mathematical proofs, indeed) and alerts developers at design time that some code they've written is heading down a very slippery slope that will end in a hang. Terminator is proof based. OK. How does Terminator work, you ask? Proofs? It's all about prooving termination.

Please tune in and find out. This is a really cool introduction to the notion of mathematically prooving that good things will eventually happen in code.

PS. I just found out that, like myself, Byron is an Evergreen State College alumnus. Small world!



Available formats for this video:

Actual format may change based on video formats available and browser capability.

    The Discussion

    Comments closed

    Comments have been closed since this content was published more than 30 days ago, but if you'd like to send us feedback you can Contact Us.