CS&E Colloquium: Automated Reasoning at Cloud Scale

The computer science colloquium takes place on Mondays from 11:15 a.m. - 12:15 p.m. This week's speaker, Mike Whalen (Amazon Web Services), will be giving a talk titled "Automated Reasoning at Cloud Scale"

Abstract

Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using proof engines called SAT and SMT solvers more than one billion times a day, both for real-time queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Reaching this scale requires that we consistently focus on our customers and provide measurable improvements for existing customer problems.  It also requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will discuss these aspects and, more generally, steps to make automated reasoning successful in a commercial organization.

Biography

Dr. Michael Whalen is a Principal Applied Scientist at Amazon Web Services and the former Director of the University of Minnesota Software Engineering Center.  Dr. Whalen is interested in formal analysis, language translation, testing, and requirements engineering.  He has led development of simulation, translation, testing, and formal analysis tools for both programming languages: Java, Rust, and C, and Model-Based Development languages: Simulink, Stateflow, and SCADE. Dr. Whalen has published 99 peer-reviewed articles on these topics, including 3 ICSE distinguished papers.  Dr. Whalen has led successful formal verification projects on real-time operating systems, foundational Amazon C libraries, and several industrial avionics projects.  He is currently working on formal verification at “cloud scale”, looking at how to scale testing and proof tools to larger and more complex problems than are handled by current tools.  He is also involved with outreach, helping developers and business customers apply verification tools to improve their team’s quality, velocity, and innovation.