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.