Automatically Proving That Computer Programs Do What They are Supposed to Do
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 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, http://mmjb.github.io/T2/, http://research.microsoft.com/en-us/projects/slam and http://biomodelanalyzer.research.microsoft.com/)
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.