Byron Cook: Terminator - Proving Good Things Will Eventually Happen

Posted By: Charles | Jul 12th, 2007 @ 8:31 AM | 12,908 Views | 6 Comments
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!
Media Downloads:
Rating:
0
0
#Jul 13th, 2007 @ 12:11 AM
keeron
keeron
Obsessive Geek

Very interesting... (although, would've loved a "deep dive" type of thing where we could get some white boarding / demos).

Any research paper / samples (even better - existing technologies) on this subject?

#Jul 13th, 2007 @ 1:25 AM
rizzo
rizzo

I had the same question and then found these links, which have pointers to papers:

http://research.microsoft.com/~bycook
http://research.microsoft.com/terminator



#Jul 13th, 2007 @ 6:57 AM
Tominator2005
Tominator2005
I'm really sorry, but since the topic of this video is programming and C++ related. I just had to say this.

this^->AddressOfPapers = %here; // \/

http://research.microsoft.com/~bycook
http://research.microsoft.com/terminator


And yes I know, I really have got too much time on my hands.
But when your unemployed,  thats life.

Im going to watch the video later.

Im interested in all programming languages, I've tried everything from Pascal to C++.

Many Thanks
Tom
#Jul 13th, 2007 @ 7:34 AM
Charles
Charles
Welcome Change
These links are provided in the description text....
#Jul 16th, 2007 @ 12:11 PM
Charles
Charles
Welcome Change
keeron wrote:


Very interesting... (although, would've loved a "deep dive" type of thing where we could get some white boarding / demos).

Any research paper / samples (even better - existing technologies) on this subject?



Byron will be in Redmond this summer and I'll do a Going Deep episode with him on Terminator. That ought to provide the "deep dive" you're looking for.
C
#Sep 27th, 2007 @ 12:08 AM
tolaat
tolaat

This Byron is a cool guy.

Liveness is not dead - it just smells funny.

Microsoft Communities