Professor of Computer Science
Byron Cook is Professor of Computer Science at University College London (UCL) and
Senior Principal at Amazon Web Services.
Byron's interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. Byron is the founder and leader of
Amazon's Automated Reasoning Group (ARG).
Highlights and some history
For publically available information on
Amazon's Automated Reasoning Group, the best place to start is to read:
Byron was a researcher at Microsoft Research (joint appointment with UCL) from 2004-2014. Check out Byron's old Microsoft Research website.
At Microsoft Research Byron started the TERMINATOR project, which made a program termination prover that worked on industrially relevant programs, such as Windows device drivers. TERMINATOR lives on
outside of Microsoft as an open-source project called T2. For a presentation about this work
watch this lecture. Just for
fun you can watch Byron giving a live demo of TERMINATOR in this
Byron was also a founding member of the Bio Model Analyzer (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 2002-04,
Byron developed a Windows product called Static Driver Verifier, which used SLAM to automatically finds bugs in Windows OS device drivers.
Before joining Microsoft, Byron worked at Prover Technology, where he helped develop and
apply the symbolic model checker
Prover SL, and SAT solver
These tools were used commercially in a variety of applications, including the verification of microprocessors, aircraft software, railway switching, and embedded systems.
Byron's first taste of industrial formal verification was back in
1998-99 when he worked at
Intel's Strategic CAD Labs (archived).
Shape analysis for composite data structures Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies, and Hongseok Yang CAV'07 [International Conference on Computer-Aided Verification] (Berlin)
Proving termination by divergence Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric SEFM'07 [ International Conference on Software Engineering and Formal Methods] (London)
Shape analysis by graph decomposition Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv TACAS'07 [International Conference on Tools and Algorithms for the Construction and Analysis of Systems] (Braga)
Thorough static analysis of device drivers Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner EuroSys'06 [European Systems Conference] (Leuven)
Design automation with mixtures of proof strategies for propositional logic Gunnar Andersson, Per Bjesse, Byron Cook and Ziyad Hanna IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 22(8) 2003
A proof engine approach to solving combinational design automation problems Gunnar Andersson, Per Bjesse, Byron Cook, and Ziyad Hanna DAC'02 [Design Automation Conference] (Las Vegas)
A framework for microprocessor correctness statements Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones International Journal on Software Tools for Technology Transfer, Vol. 4(3), 2003
A framework for microprocessor correctness statements Mark Aagaard, Byron Cook, Nancy Day, and Robert Jones CHARME'01 [Correct Hardware Design and Verification Methods] (Edinburgh)
Combining stream-based and state-based verification techniques for microarchitectures Mark Aagaard, Byron Cook, and Nancy Day FMCAD'00 [International Conference on Formal Methods in Computer Aided Design] (Austin)
Formal verification of explicitly parallel microprocessors Byron Cook, John Launchbury, John Matthews, and Dick Kieburtz CHARME'99 [Conference on Correct Hardware Design and Verification Methods] (Bad Herrenalb)
On embedding a microarchitectural design language within Haskell John Launchbury, Jeff Lewis and Byron Cook ICFP'99 [International Conference on Functional Programming] (Paris)
Specifying superscalar microprocessors in Hawk Byron Cook, John Launchbury, and John Matthews 1998 Workshop on Formal Techniques for Hardware (Marstrand)
Microprocessor specification in Hawk John Matthews, John Launchbury, and Byron Cook ICL'98 [International Conference on Computer Languages] (Chicago)
Disposable memo functions Byron Cook and John Launchbury 1997 Haskell Workshop Proceedings (Amsterdam)