Software plays an increasing role in the operation of critical systems. As these systems become more complex, ensuring software correctness becomes much more difficult. I am interested in automated formal techniques for precisely specifying, implementing, and verifying software. To support these activities, I have developed several translation and analysis tools to support formal reasoning and test case generation. I have significant experience in applying formal verification and auto-test generation techniques to production DO178B Level A and B avionics software development efforts.
I am a part of the Critical Systems Group (CriSys) whose research interests are in the general area of software engineering; in particular, software development for critical software applications - applications where incorrect operation of the software could lead to loss of life, substantial material or environmental damage, or large monetary losses. The long-term goal of our research activities is the development of a comprehensive framework for the development of software for critical software systems. Our work has focused on some of the most difficult and least understood aspects of software development - requirements specification and validation/verification. For more information, and possible student research opportunities please visit the
Crisys Group Page.
A list of my publications can be found
- Fall 2010, 2011, 2012 - SEng 5861: Software Architecture
- Spring 2007 - SEng 5841: Model-Based Software Development and Analysis
- My Curriculum Vitae is available here.
- Positions held:
6-254 Keller Hall (formerly EE/CSci Building),
a map to Keller Hall.
6-208 Keller Hall
Michael W. Whalen
Dept. of Computer Science and Engineering
4-192 Keller Hall
University of Minnesota
200 SE Union Street
Minneapolis, MN 55455
+1 612 624 5130 - office
+1 612 625 0572 - fax