Microsoft Research
Microsoft Translator |
Byron Cook

Dr. Byron Cook is a Principal Researcher at Microsoft's laboratory at Cambridge University where he manages the Programming Principles and Tools (PPT) group together with Andy Gordon.  Byron is also full professor of computer science at University College London (UCL) . 

Research

Byron's research interests include program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems.  Byron's recent work has been focused on the development of automatic tools for proving program termination/liveness (see the TERMINATOR project), memory safety (see the SLAyer project), as well as properties about models of biological systems (see the BMA project). 

Students

Former PhD students: Alexey Gotsman and Eric Koskinen. Current PhD student: Kaustubh Nimkar.

Interns

Byron's current and past MSR interns include: Aws Albarghouthi, Mary Boeker, Marc Brockschmidt, Hongyi Chen, Ashutosh Gupta, Mihaela Gheorghiu, Alexey Gotsman, Christoph Haase, Zachary Kincaid, Heidy Khlaaf, Matt Lewis, Shuvendu Lahiri, Stephen Magill, Andrei Popescu, Patrick Rondon, Andrey Rybalchenko, Abigail See, Vlad Shcherbina, Jiri Simsa, Thomas Stroeder, Viktor Vafeiadis, Georg Weissenbacher, Thomas Wies, and Greta Yorsh.

Visitors

Byron sometimes hosts visits by professors.  Current and past visiting professors include Koen Claessen, 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.

Still want more information?

You can find out all of the details about Byron 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
    Microsoft Research
    21 Station Road
    Cambridge, CB1 2FB
    United Kingdom