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 theorem proving, logic, program analysis/verification, and programming languages. Byron
has applied these techniques to domains such as GenAI, distributed systems, hardware, 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
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
PhD dissertation
Still want more information?
You can find out all of the details about Byron in his CV/Resume.