Prof. Dr. Byron Cook, FREng
Contact: byroncook@gmail.com

Byron Cook is Professor of Computer Science at University College London (UCL). Byron is also Vice President and Distinguished Scientist at Amazon and AWS. Byron's interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems.

Highlights and some history

Byron drove the broad adoption of formal methods and automated reasoning now in use at Amazon. For more information see a recent talk called The business of proof, an interview with Werner Vogels, an interview from PLDI, a short interview on the Cube, Amazon SVP Peter DeSantis' re:invent keynote, or a FLoC'18 keynote lecture. See https://www.amazon.science/research-areas/automated-reasoning for papers from Amazon in this space.

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 interview.

Byron used to hang out a lot with the East London Massive.

Byron was a founder of the SLAyer project (github). SLAyer was one of the forerunners to the Infer tool

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.

Byron, together with Shuvendu Lahiri started Microsoft's first SMT decision procedure project, called Zapato. Zapato was the decision procedure used in the initial release of 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 helped develop and apply the symbolic model checker Prover SL, and SAT solver Prover CL. 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).

Publications

Generating and Exploiting Automated Reasoning Proof Certificates

Haniel Barbosa, et. al

CACM 2023

Partitioning Strategies for Distributed SMT Solving

Amalee Wilson, et. al

FMCAD 2023

Model checking boot code from AWS data centers

Byron Cook, et. al

FMSD 57(1):34-52 (2021)

Code-level model checking in the software development workflow at Amazon Web Services

Nathan Chong, et. al

SPE 51(4):772-797 (2021)

Stratified Abstraction of Access Control Policies

John Backes, et. al

CAV 2020

Using model checking tools to triage the severity of security bugs in the Xen hypervisor.

Byron Cook, et. al

FMCAD 2020

Block Public Access: Trust Safety Verification of Access Control Policies

Malik Bouchet, et. al

ESEC/FSE 2020

Model checking boot code from AWS data centers (extended version)

B. Cook, K. Khazem, D. Kroening, S. Tasiran, M. Tautschnig and M. Tuttle.

Journal of Formal Methods in Systems Design (2020)

One-click formal methods

John Backes, et. al

IEEE Software Magazine, November/December 2019

Reachability Analysis for AWS-based Networks

John Backes, et. al

CAV 2019

Formal reasoning about the security of Amazon Web Services

Byron Cook

CAV 2018

Model checking boot code from AWS data centers

B. Cook, K. Khazem, D. Kroening, S. Tasiran, M. Tautschnig and M. Tuttle.

CAV 2018

Continuous formal verification of Amazon s2n

Andrey Chudnov, et. al

CAV 2018

Semantic-based Automated Reasoning for AWS Access Policies using SMT

John Backes, et. al

FMCAD 2018

SideTrail: Verifying Time-Balancing of Cryptosystems

K. Athanasiou, B. Cook, M. Emmi, C. MacCarthaigh, D. Schwartz-Narbonne and S. Tasiran

VSTTE 2018

Verifying increasingly expressive temporal logics for infinite-state systems

B. Cook, H. Khlaaf, and N. Piterman.

Journal of the the ACM, 64, 2, Article 15 (May 2017), 39 pages.

T2: Temporal property verification

M. Brockshmidt, B. Cook, S. Ishtiaq, H. Khlaaf, and N. Piterman.

TACAS 2016

Learning to decipher the heap for program verification

Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, and Daniel Tarlow.

Workshop on Constructive Machine Learning at ICML 2015.

Drug target optimization in chronic myeloid leukemia using innovative computational platform

R. Chuang, B. Hall, D. Benque, B. Cook, S. Ishtiaq, N. Piterman, A. Taylor, M. Vardi, S. Koschmieder, B. Gottgens, and J. Fisher

Scientific Reports, 5:8190, Nature Publishing Group, February 2015

On Automation of CTL* Verification for Infinite-State Systems

B. Cook, H. Khlaaf, and N. Piterman.

CAV 2015

Fairness for infinite-state systems

B. Cook, H. Khlaaf, and N. Piterman.

TACAS 2015

Spatial Interpolants

A. Albarghouthi, J. Berdine, B. Cook, and Z. Kincaid

ESOP 2015

Relations

Tauba Auerbach, Byron Cook, David Reinfurt

Bulletins of the Serving Library

Disproving termination with overapproximation

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter O'Hearn

FMCAD 2014

Faster temporal reasoning for infinite-state programs

Byron Cook, Heidy Khlaaf, Nir Piterman

FMCAD 2014

Proving nontermination via safety

Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter O'Hearn

TACAS 2014

Finding instability in biological models

Byron Cook, Jasmin Fisher, Benjamin Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman

CAV 2014

Mathematical artifacts (re: Tauba Auerbach)

Byron Cook

Parkett 94, 2014

Better termination proving through cooperation

Marc Brockschmidt, Byron Cook, Carsten Fuhs

CAV 2013

Reasoning about nondeterminism in programs

Byron Cook and Eric Koskinen

PLDI 2013

Ramsey vs. lexicographic termination proving

Byron Cook, Abigail See, and Florian Zuleger

TACAS 2013

At the interface of biology and computation

Alex S. Taylor, Nir Piterman, Samin Ishtiaq, Jasmin Fisher, Byron Cook, Caitlin Cockerton, Sam Bourton, David Benque

CHI 2013

Ranking function synthesis for bit-vector relations

Byron Cook, Daniel Kroening, Philipp Rummer, Christoph Wintersteiger

Formal Methods in System Design, 2013

Proving termination of nonlinear command sequences

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric

Formal Aspects of Computing (special issue from SEFM), 2013

BMA: Visual Tool for Modeling and Analysis of Biological Networks (tool paper)

David Benque, Sam Bourton, Caitlan Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor, Moshe Vardi

CAV 2012

Temporal property verification as a program analysis task (extended version)

Byron Cook, Eric Koskinen, Moshe Vardi

Formal Methods in System Design (special issue from CAV), 2012

Proving program termination (Review article)

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Communications of the ACM, Volume 54 Issue 5, May 2011

Temporal property verification as a program analysis task

Byron Cook, Eric Koskinen, Moshe Vardi

CAV'11 [International Conference on Computer-Aided Verification] (Snowbird)

SLAyer: Memory safety for systems-level code

Josh Berdine, Byron Cook, Samin Ishtiaq

CAV'11 [International Conference on Computer-Aided Verification] (Snowbird)

Making prophecies with decision predicates

Byron Cook and Eric Koskinen

POPL'11 [Symposium on Principles of Programming Languages] (Austin)

Tractable reasoning in a fragment of separation logic

Byron Cook, Christoph Hasse, Joel Ouaknine, Matthew Parkinson, James Worrell

CONCUR'11 [International conference on concurrency theory] (Aachen)

Proving stabilization of biological systems

Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman

VMCAI'11 [Verification, model checking, and abstract interpretation] (Austin)

Precision and the conjunction rule in concurrent separation logic

Alexey Gotsman, Josh Berdine, Byron Cook

MFPS'11 [Conference on the Mathematical Foundations of Programming Semantics] (Pittsburgh)

Ranking function synthesis for bit-vector relations

Byron Cook, Daniel Kroening, Philipp Rummer, and Christoph Wintersteiger

TACAS'10 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems]

Finding heap-bounds for hardware synthesis

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis

FMCAD'09 [Formal Methods in Computer Aided Design] (Austin)

Summarization for termination: No return!

Byron Cook, Andreas Podelski, Andrey Rybalchenko

FMSD (2009) 35:369-387

Proving that non-blocking algorithms don't block

Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis

POPL'09 [Symposium on Principles of Programming Languages] (Savannah)

Principles of program termination(DRAFT)

Byron Cook

Notes from the 2008 Marktoberdorf summer school

Proving conditional termination

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv

CAV'08 [International Conference on Computer-Aided Verification] (Princeton)

Scalable shape analysis for systems code

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn

CAV'08 [International Conference on Computer-Aided Verification] (Princeton)

Ranking abstractions

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang

ESOP'08 [European Symposium on Programming] (Budapest)

Verification of Boolean programs with unbounded thread creation

Byron Cook, Daniel Kroening, and Natasha Sharygina

Journal of Theoretical Computer Science, Vol. 388, 2007, pp. 227-242

Predicate abstraction via symbolic decision procedures

Shuvendu Lahiri, Thomas Ball and Byron Cook

Journal of Logical Methods in Computer Science, Vol. 3, 2007, pp. 1-20

Proving thread termination

Byron Cook, Andreas Podelski, and Andrey Rybalchenko

PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

Thread-modular shape analysis

Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv

PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)

Local reasoning for storable locks and threads

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv

APLAS'07 [Asian Symposium on Programming Languages and Systems] (Singapore)

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)

Arithmetic strengthening for shape analysis

Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook.

SAS'07 [International Static Analysis Symposium] (Denmark)

Proving that programs eventually do something good

Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi

POPL'07 [Symposium on Principles of Programming Languages] (Nice)

Variance analyses from invariance analyses

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn

POPL'07 [Symposium on Principles of Programming Languages] (Nice)

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)

Automatic termination proofs for programs with shape-shifting heaps

Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn

CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Terminator: Beyond safety(short tool description paper)

Byron Cook, Andreas Podelski, and Andrey Rybalchenko

CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Repair of Boolean programs with an application to C

Andreas Griesmayer, Roderick Bloem, and Byron Cook

CAV'06 [International Conference on Computer-Aided Verification] (Seattle)

Termination proofs for systems code

Byron Cook, Andreas Podelski, and Andrey Rybalchenko

PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)

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)

Over-approximating Boolean programs with unbounded thread creation

Byron Cook, Daniel Kroening, Natasha Sharygina

FMCAD'06 [Formal Methods in Computer Aided Design] (San Jose)

Interprocedural shape analysis with separated heap abstractions

Alexey Gotsman, Josh Berdine, and Byron Cook

SAS'06 [International Static Analysis Symposium] (Seoul)

Abstraction refinement for termination

Byron Cook, Andreas Podelski, Andrey Rybalchenko

SAS'05 [International Static Analysis Symposium] (London)

Using Stalmarck's algorithm to prove inequalities

Byron Cook, Georges Gonthier

ICFEM'05 [International Conference on Formal Engineering Methods] (Manchester)

Symbolic model checking for asynchronous Boolean programs

Byron Cook, Daniel Kroening, Natasha Sharygina

SPIN'05 (San Francisco)

Predicate abstraction via symbolic decision procedures

Shuvendu Lahiri, Thomas Ball and Byron Cook

CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)

Cogent: Accurate theorem proving for program verification(short tool description paper)

Byron Cook, Daniel Kroening, Natasha Sharygina

CAV'05 [International Conference on Computer-Aided Verification] (Edinburgh)

Zapato: Automatic theorem proving for predicate abstraction refinement(short tool description paper)

Thomas Ball, Byron Cook, Shuvendu K. Lahriri, and Lintao Zhang

CAV'04 [International Conference on Computer-Aided Verification] (Boston)

Refining approximations in software predicate abstraction

Thomas Ball, Byron Cook, Satyaki Das, and Sriram K. Rajamani

TACAS'04 [Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems]

A symbolic approach to predicate abstraction

Shuvendu K. Lahiri, Randal E. Bryant, and Byron Cook

CAV'03 [International Conference on Computer-Aided Verification] (Boulder)

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)

Past and current projects

Automated Reasoning Group (ARG) IAM Access Analyzer Tiros Zelkova

T2 and the original TERMINATOR (archived)

East London Massive (archived)

Bio Model Analyzer (BMA)

SLAyer

Static Driver Verifier

SLAM

Prover SL (archived)

Prover CL (archived)

Hawk (archived)

Press

Next Generation Security with Automated Reasoning, an Artificial Intelligence Technology

AWS Podcast #266

Amazon tests out two tools to help keep its cloud secure

Wired magazine

By Lily Hay Newman

July, 2018

How Do You Explain The Unreasonable Effectiveness Of Cloud Security?

highscalability.com,

September 2018

Amazon Adds Crypto-Based Security Tools

pymnts.com,

September 2018

Why the blue screen of death no longer plagues Windows users

ZDNet

By Nick Heath

September, 2013

Computing Cancer

Nature

By Neil Savage

November, 2012

Geek of the week

Simple Talk

By Richard Morris

September, 2010

A Sign of the Times

Wired

By Cameron Bird

December, 2009

A Good Sign

Science

By Angela Saini

July, 2009

Optic Nerve

Vogue

By Dodie Kazanjain

January, 2009

All Shook Down

San Francisco Weekly

By Hiya Swanhuyser

December 28, 2008

Inside Terminator

channel9.msdn.com

By Charles Torre

September, 2007

Using Proofs to Catch System Hangs Before They're Born

channel9.msdn.com

By Charles Torre

July, 2007

Send in the Terminator

By Gary Stix

Scientific American

December, 2006

Testers aim to kill off dreaded blue screens

By Mary Branscombe

Financial Times

November, 2006

Terminator tackles an impossible task

By Rob Knies

Microsoft Research News

September, 2006

Microsoft bug-checking tools promise fewer crashes

By Joris Evers

CNET

May, 2006

Microsoft's secret bug squasher

By Simson Garfinkel

Wired

November, 2005

Building a better bug-trap

The Economist

June, 2003

Researching a path to fewer bugs

By Patrick Meader

Visual Studio Magazine

February, 2003

Recorded presentations

Formal reasoning about the security of Amazon Web Services

Place: FLoC Plenary

Date: July 16, 2018

Materials: Video Formal reasoning about the security of Amazon Web Services

Place: OOPSLA/SPLASH 2018 keynote lecture

Date: November 9, 2018

Materials: Video

Automated Formal Reasoning About AWS Systems

Place: AWS Re:Invent

Date: November 29, 2016

Materials: Video

Automatically Proving Program Termination (and more)

Place: University of Colorado

Date: October 24, 2013

Materials: Video

We can prove termination. Now what?

Place: Workshop on Software Correctness and Reliability 2013

Date: October 7, 2013

Materials: Video

Automatically Proving Concurrent Programs Correct

Place: Microsoft TechFest'07

Date: March 8th 2007

Materials: Video

Variance Analyses from Invariance Analyses

Place: Microsoft Research, Redmond

Date: August 8th 2006

Materials: Video

Automatically proving the termination of C programs

Place: Isaac Newton Institute for Mathematical Sciences

Date: February 3rd 2006

Materials: slides and audio

Applications of Automated Reasoning

Place: Microsoft TechFest'05

Date: March 8th 2005

Materials: Video

PhD dissertation

Structuring instruction-sets with higher-order functions

Still want more information?