Dr. Michael Whalen is a Sr. Software Engineer interested in formal analysis, compilers, testing, and requirements engineering. He has 15 years experience in software development and analysis, including 10 years experience in Model-Based Development. He has developed simulation, translation, testing, and formal analysis tools for MBD languages including Simulink, Stateflow, Lustre, and RSML-e, and has published over 20 papers on these topics. He has led successful industrial formal verification projects on commercial avionics displays (ADGS-2100 Window Manager), security (High Speed Crypto Controller (HSCC)), adaptive flight control (Air Force Research Labs/Lockheed Martin CerTA FCS) and autoland (CerTA CPI) software. 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 has been an engineer at Rockwell Collins since 2003.