Share this page
  • Share this page on Twitter Share this page on Facebook Share this page on Digg Share this page on Del.icio.us Read the Inside Microsoft Research blog
  • E-mail this page Print this page
  • RSS feeds
Home > People > Byron Cook
Byron Cook

Dr. Byron Cook is a Principal Researcher at Microsoft's laboratory at Cambridge University where he leads the Verification and Automated Reasoning Group.  Byron is also full professor of computer science at Queen Mary, University of London. 

Research

Byron's research interests include program analysis/verification, programming languages, theorem proving, logic, hardware design, and operating systems.  Byron's recent work has been focused on the development of automatic tools for

Teaching

Byron has recently taught graduate-level courses on methods of proving program termination at Berkeley, Cambridge, Carnegie Mellon, Imperial College, the Marktoberdorf summer school, and the Trends in Concurrency summer school. Annotated copies of the slides from the Marktoberdorf lectures will be made available soon. The lecture notes from these courses will form the basis of Byron's forthcoming book, entitled Proving Program Termination (Cambridge University Press).

Students

Byron supervises several PhD students at Cambridge University, including Alexey Gotsman and Eric Koskinen. Byron sometimes also supervises Cambridge undergraduate final-year projects.

Interns

Byron's current and past research interns include: Ashutosh Gupta, Mihaela Gheorghiu, Alexey Gotsman, Shuvendu Lahiri, Jacopo Mantovani, Stephen Magill, Andrei Popescu, Patrick Rondon, Andrey Rybalchenko, Jiri Simsa, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh.

Visitors

Byron sometimes hosts visits by professors.  Current and past visiting professors include Peter O'Hearn, Andreas Podelski, John Reynolds, Mooly Sagiv, Moshe Vardi, and Helmut Veith.

History

  • Byron 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.
  • Byron, together with Shuvendu Lahiri 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, Byron worked at Prover Technology, where he 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.
  • Byron's PhD is from OGI, where he 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 invented while working both on the Motorola Advanced INFOSEC Machine and prototypes of Intel microprocessors while at Intel's Strategic CAD Research Laboratories.

You can find out more information about Byron on his blog or in his CV. 

Publications

Projects

Upcoming events

Press

Recorded presentations

Contact

  • Admin: Lynn Hammans
  • Email: a-lynnh@microsoft.com 
  • Telephone: +44 1223 479 943
  • Fax: +44 1223 479 999
  • Regular mail:
    Byron Cook
    Roger Needham Building
    J J Thomson Avenue
    Cambridge, CB3 0FB
    United Kingdom