Byron Cook: Inside Terminator
- Posted: Sep 13, 2007 at 2:24 PM
- 17,064 Views
- 8 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)
A few months ago, I
interviewed
Byron Cook, a researcher at
MSR Cambridge, about his work on
Terminator, which is a proof-based analysis tool used for proving that good things will eventually happen in unmanaged code paths. That is, it's a very good thing for code to stop executing eventually otherwise system hangs occur (drivers are the number
one cause of system hangs and other undesirable system-wide problems).
Terminator is designed to help developers find bugs in their code that cause non-terminating execution. Many of you provided feedback after the last interview that Byron should have gone a bit deeper into the technology, including whiteboarding proofs. Well, he was recently in Redmond and agreed to be the next participant in Going Deep.
Here we dig into the details of Terminator on the whiteboard and even see a demo of Terminator running over some DDK (Driver Development Kit) sample C code.
Fasten your seat belts. We do jump head first into the rabbit hole.
Enjoy!
PS: The Download file (pointed to from the Download button below) was encoded at 512Kbs. If you want a higher bit rate file you can click here.
Terminator is designed to help developers find bugs in their code that cause non-terminating execution. Many of you provided feedback after the last interview that Byron should have gone a bit deeper into the technology, including whiteboarding proofs. Well, he was recently in Redmond and agreed to be the next participant in Going Deep.
Here we dig into the details of Terminator on the whiteboard and even see a demo of Terminator running over some DDK (Driver Development Kit) sample C code.
Fasten your seat belts. We do jump head first into the rabbit hole.
Enjoy!
PS: The Download file (pointed to from the Download button below) was encoded at 512Kbs. If you want a higher bit rate file you can click here.
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
It looks like there will soon be very few excuses for not having reliable device drivers at least though!
you might want to read up a bit on ada and spark: it's a fascinating world for die-hard c++ programmers especially.
cheers,
martin
Anyways, Byron made a typo:
he was trying to prove
(x>0 && y>0 && x`=x && y`=y-1)
||
(x>0 && y>0 && y`=y-1 && x`=x)
what should be is the following, because the above two are the same, unless I forgot boolean algebra:
(x>0 && y>0 && x`=x && y`=y-1)
||
(x>0 && y>0 && x`=x-1 && y`=y)
Great stuff, I miss that in my day-to-day .NET life
You mention a great blog article by a Chris Broom in the video, but I'm unable to find it. Do I have the name right? Can someone post a link?
Thanks,
Jason
Remove this comment
Remove this thread
close