Michael Whalen

Registered user since Mon 31 Oct 2016

Name:Michael Whalen
Bio:

Dr. Michael Whalen is a Principal Applied Scientist at Amazon Web Services and the former Director of the University of Minnesota Software Engineering Center. He has more than 25 years of experience in software development and analysis, including 15 years of experience in Model-Based Development & safety-critical systems. Dr. Whalen has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. He has led successful large-scale formal verification projects on industrial avionics systems, including displays (Rockwell-Collins ADGS-2100 Window Manager, deployed on the Boeing 787), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). Dr. Whalen was the lead developer of the Rockwell-Collins Gryphon tool suite, which was used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. He is currently working on the AGREE tool suite for architectural analysis and testing in AADL, which was recently used to verify correct system behavior in the Boeing Little Bird autonomous helicopter as part of the DARPA HACMS project.

Dr. Whalen is a frequent speaker and author on the use of formal methods and automated testing, with 44 invited presentations, 16 journal publications, one book chapter, 72 conference and workshop papers, and 12 contractor and technical reports published. He has two ICSE and one DASC distinguished papers related to testing, as well as three distinguished papers related to novel uses of model checking. His PhD dissertation involved using higher-order abstract syntax as a basis for a provably-correct code generation tool from the RSML-e specification language into a subset of C. He is currently working on formal verification at “cloud scale”, looking at how to create proof engines that can cost-effectively scale 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.

Country:United States
Affiliation:Amazon Web Services and the University of Minnesota
Research interests:SAT, SMT, Model Checking, Testing, Requirements

Contributions

ICSE 2024 Committee Member in Research Track within the Research Track-track
Requirements Engineering 2023 Industrial Innovation Track Co-Chair in Organizing Committee
Industrial Innovation Track Co-Chair in Program Committee within the Industrial Innovation Papers-track
ICSE 2022 Committee Member in Program Committee within the Technical Track-track
REFSQ 2022 Author of Requirements, Models, and Automated Reasoning in the Cloud. within the Research Papers-track
ICSE 2021 Sustainability Chair in Organizing Committe
Committee Member in Program Committee within the Technical Track-track
VMCAI 2021 Committee Member in Program Committee within the VMCAI-track
ESEC/FSE 2020 Author of Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java within the Research Papers-track
ASE 2020 Author of Synthesis of Infinite-State Systems with Random Behavior within the Research Papers-track
ICSE 2020 Committee Member in Program Committee within the New Ideas and Emerging Results-track
Programme Committee in Program Committee within the Software Engineering in Practice-track
FormaliSE 2020 PC Member in Program Committee within the FormaliSE 2020-track
VMCAI 2020 Author of Panel "The Future of Software Verification" at VMCAI within the VMCAI 2020-track
ASE 2019 Committee Member in Program Committee within the Research Papers-track
Committee Member in Steering Committee
ICSE 2019 SEIP Chair in Program Committee within the Software Engineering in Practice-track
Session Chair of Managing Variation: An Industrial Perspective on Product Line Engineering (part of Plenary)
Committee Member in Program Committee within the ACM Student Research Competition-track
Author of IEEE Software Best Software Engineering in Practice Award within the Plenary-track
SEIP Chair in Organizing Committee
Author of Opening Ceremonies within the Plenary-track
FormaliSE 2019 Committee Member in Program Committee within the FormaliSE 2019-track
HILT 2018 Committee Member in Program Committee within the HILT 2018-track
* ICSE 2018 * Committee Member in Program Committee within the NIER - New Ideas and Emerging Results -track
Committee Member in Program Committee within the TB - Technical Briefings -track
Session Chair of Security, Safety, and Quality (part of NIER - New Ideas and Emerging Results )
FormaliSE 2018 Session Chair of Formal Methods for Autonomous Systems 2 (part of FormaliSE 2018)
Committee Member in Program Committee within the FormaliSE 2018-track
ISSTA 2017 Keynote Speaker of Keynote Talk: Test Metrics and Generation Strategies for Next-Generation CPS Software within the TECPS-track
Committee Member in Organizing Committee within the TECPS-track
SPIN 2017 Committee Member in Program Committee