Byron Cook
Professor of Computer Science

Byron Cook is Professor of Computer Science at University College London (UCL). Byron is also a Senior Principal at Amazon.


Byron's research interests include program analysis/verification, security, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. At Amazon Byron leads a research group focused on formal/constraint-based tools for reasoning about cloud-computing security.


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

Current PhD student: Heidy Khlaaf


Byron's current and past 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.


  • Byron was a researcher at Microsoft Research (joint appointment with UCL) from 2004-2014. During 2002-2004 Byron was a software developer in the Microsoft Windows OS kernel team.
  • At Microsoft Research Byron started the TERMINATOR program termination project, which continues outside of Microsoft as an open-source project called T2.
  • Byron was a founder of Microsoft's SLAyer project, which developed a tool capable of automatically proving properities of programs that make non-trivial use of the heap.
  • Byron was also a founding memboer of the BMA project, which developed a tool that facilitates the modelling and analysis of genetic signalling pathways.
  • Byron was one of the developers of the SLAM software model checker. As a member of the Windows OS kernel team Byron helped developed a Windows product called Static Driver Verifier, which used SLAM to 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 (a.k.a. Resume).


Upcoming events


Recorded presentations