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: Shuvendu Lahiri, Andrey Rybalchenko, Georg Weissenbacher, Jacopo Mantovani, Stephen Magill, Alexey Gotsman, Viktor Vafeiadis, 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.

Service. While I'm trying not to take on too much service work, I am currently involved in the administration of the following upcoming conferences:

• POPL'08 (PC)
• TACAS'08 (PC)
• CAV'08 (Workshops chair)
• CAV'10 (Co-chair)

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.