Byron Cook
Professor of Computer Science



Byron is a professor of computer science (joint appointment with Microsoft Research) at Queen Mary, University of London, where he works with the East London Massive. Byron's research interests include program verification, symbolic model checking, automatic theorem proving, and programming language theory. Byron has recently been working on
  • Automatic methods of proving program termination (see the TERMINATOR project),
  • Counterexample-guided abstraction refinement for concurrent programs,
  • Tools for proving properties about programs that modify the heap (see the SLAyer project).

Byron is one of the researchers who developed the SLAM software model checker, which is used in Microsoft's Static Driver Verifier product.

Byron's PhD is from OGI. His undergraduate degree is from Evergreen.

For more information see Byron's webpage at Microsoft Research, his blog, and his CV.