Byron Cook: Terminator - Proving Good Things Will Eventually Happen
- Posted: Jul 12, 2007 at 8:31 AM
- 13,548 Views
- 6 Comments
Download
How do I download the videos?
- To download, right click the file type you would like and pick “Save target as…” or “Save link as…”
Why should I download videos from Channel9?
- It's an easy way to save the videos you like locally.
- You can save the videos in order to watch them offline.
- If all you want is to hear the audio, you can download the MP3!
Which version should I choose?
- If you want to view the video on your PC, Xbox or Media Center, download the High Quality WMV file (this is the highest quality version we have available).
- If you'd like a lower bitrate version, to reduce the download time or cost, then choose the Medium Quality WMV file.
- If you have a Zune, WP7, iPhone, iPad, or iPod device, choose the low or medium MP4 file.
- If you just want to hear the audio of the video, choose the MP3 file.
Right click “Save as…”
- MP3 (Audio only)
- Mid Quality WMV (Lo-band, Mobile)
- WMV (WMV 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!
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!
Comments Closed
Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation,
please create a new thread in our Forums,
or
Contact Us and let us know.
Follow the Discussion
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?
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
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
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
This Byron is a cool guy.
Liveness is not dead - it just smells funny.
Remove this comment
Remove this thread
close