Dr. Michael W. 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 C, Rust, and Model-Based Development languages including Simulink, Stateflow, SCADE, and RSML-e, and has published 85 peer-reviewed articles on these topics. Dr. Whalen has led successful formal verification projects on foundational Amazon C libraries and large industrial avionics models, including secure autonomous vehicles (DARPA HACMS project), pilots’ displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program).  He is currently working on formal verification at “cloud scale”, part of a team that runs thousands of proofs on C and Rust code every day.  He is working on improving the scalability of formal verification and extracting information from proofs to satisfy compliance and certification requirements.