Byron Cook

---

I am a researcher at Microsoft's laboratory at Cambridge University and an industrial fellow at Cambridge University. I will spend a sabbatical at Carnegie Mellon University during the spring semester of 2008.

Research. My research interests include program analysis/verification, programming languages, theorem proving and logic. I am especially interested in automatic methods. For the past few years I have been working on automatic program verification tools for

• Termination and liveness (See TERMINATOR and a recent Scientfic American article),
• Concurrency (See a recorded lecture from Microsoft's TechFest'07), and
• Mutable data structures (See the SLAyer project).

Teaching. I've recently taught graduate-level courses at Cambridge and Carnegie Mellon on methods of proving program termination and liveness. This summer I will be lecturing on the same topic at Imperial College, the Marktoberdorf summer school, and the Trends in Concurrency summer school.

Students. I supervise several PhD students at Cambridge University. My current students are Alexey Gotsman and Eric Koskinen. I have also supervised a number of Cambridge undergraduate final-year projects. Here are some TERMINATOR-related suggestions. Contact me if you're interested in doing a PhD or final-year project under my supervision at Cambridge.

Interns. I have a fairly steady stream of PhD students who visit me here at the Microsoft lab as interns. Current and past interns include: Mihaela Gheorghiu, Alexey Gotsman, Shuvendu Lahiri, Patrick Rondon, Andrey Rybalchenko, Jacopo Mantovani, Stephen Magill, Andrei Popescu, Jiri Simsa, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh. Please email me if you're interested in doing an internship.

Visitors. I also have a fairly steady stream of professors visiting me for 3 months at a time. Current, future, and past long-term visitors include: Peter O'Hearn, Andreas Podelski, John Reynolds, Mooly Sagiv, Moshe Vardi, and Helmut Veith.

History. Here is a brief summary of what I used to do:

• I was one of the developers of the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. I spent a year and half as the lead developer in the Static Driver Verifier project.
• Shuvendu Lahiri and I started Microsoft's first SMT decision procedure project, called Zapato. Zapato is the decision procedure currently used within SLAM. Zapato eventually led to Madan Musuvathi's Zap decision procedure, which has since been replaced by Nikolaj Bjorner and Leonardo de Moura's Z3.
• Before joining Microsoft, I worked at Prover Technology, where I investigated new algorithms for use in SAT solvers and symbolic model checking tools. These tools (Prover SL, for example) are used in a variety of applications, including the verification of microprocessors, aircraft software, and embedded systems.
• My PhD is from OGI, where I developed a programming language for describing microprocessors and invented a technique based on parametricity to decompose proofs of microprocessor correctness. The theory behind this work was motivated by tricks that I invented while working both on the Motorola Advanced INFOSEC Machine and prototypes of Intel microprocessors while I was at Intel's Strategic CAD Research Laboratories.

Here is a short biography suitable for invited lectures,etc.

You can find out much more information about me on my blog.