Automatically Proving That Computer Programs Do What They are Supposed to Do

Byron Cook

2382st Meeting Abstract
Friday, November 3, 2017 at 8:00 PM

About the Lecture

Predicting the “Unpredictable” and Killing the Blue Screen of Death

This lecture will discuss advances in tools and techniques based on mathematical logic that now allow us to prove (sometimes automatically) that computer systems are doing what they are intended to do. This work has wide application in a variety of areas such as airline and railway safety, pharmaceutical research for drug discovery, and computer and network security.


About the Speaker

Byron CookByron Cook founded and leads Amazon Web Services Security Automated Reasoning Group, which develops and applies constraint/logic based automated tools for proving the correctness of software, network configurations, and policies.  Byron also is Professor of Computer Science at University College London.  Before joining AWS, Byron was with Microsoft and with Microsoft Research. He also was  Professor of Computer Sciences at Queen Mary University, London while with Microsoft.

Byron's research focuses on functional programming, hardware modeling and design, Boolean Satisfiability Problem solving (SAT), symbolic model checking for finite-state systems, decision procedures, automatic program verification and analysis, shape analysis, and the analysis of biological systems.  He has worked on R analysis/verification, security, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems.  While with Microsoft he worked on the Windows kernel and also developed the TERMINATOR termination prover, the SLAM code analysis engine, and a variety of tools for biological analysis.  (See, respectively,, and

Byron earned a BS in Mathematics, Logic and Computer Science at The Evergreen State College and a PhD in Computer Science at the Oregon Health and Science University.

←Previous Abstract | Next Abstract → -->
Lecture Series Index - Home