Byron Cook
Program Manager
Information Innovation Office
Dr. Byron Cook joined DARPA part-time in October 2024 as part of the pilot Private Sector Personnel Program. His research interests include automated formal reasoning and programming languages.
Cook is also a professor at the University College London and a vice president and distinguished scientist at Amazon, where he founded Amazon’s Automated Reasoning Group (ARG).
Cook is perhaps best known for his work in the private sector on automatic methods for proving program termination and the Terminator termination prover. This work represented a breakthrough, challenging the prevailing opinion in computer science that automatic termination proving was impossible. Cook also contributed to Microsoft’s SLAM and the product Static Driver Verifier, often credited for reviving automatic program verification research.
Cook developed dozens of verification and security tools and has published over 80 technical papers, has keynoted dozens of conferences, and his work has gained significant media attention, with coverage in the Economist, Financial Times, Science, Scientific American, TechCrunch, Vogue, and Wired. He has received multiple awards for his research contributions, notably the Roger Needham Award and the distinction of Fellow of the Royal Academy of Engineering.
Cook holds a doctorate in computer science from the Oregon Health Sciences University and a Bachelor of Science in computer science from the Evergreen State College.