Byron Cook
Professor of Computer Science

Byron Cook is a Principal Researcher at Microsoft Research, where he splits his time between MSR-NYC and MSR-Cambridge. Byron is also full professor of computer science at University College London (UCL).


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 T2 project), memory safety (see the SLAyer project), as well as properties about models of biological systems (see the BMA project).


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


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.


  • Together with Andreas Podelski and Andrey Rybalchenko, Byron developed the TERMINATOR termination prover, which was used to prove that the dispatch routines from Windows device drivers eventually returned control back to the Windows OS. TERMINATOR was extended in numerous ways (e.g. with support for LTL). Recently Byron and others have developed a new tool that replaces TERMINATOR, called T2. The original papers on TERMINATOR and subsequent papers on T2 can be found on the T2 project webpage.
  • 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.