Michael W Whalen


Accepting PhD Students

PhD projects

AMASE: Model based safety analysis ARCHER: Compositional verification of systems-of-systems SNOW CRASH: White box fuzz testing

If you made any changes in Pure, your changes will be visible here soon.

Personal profile

Research interests

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.


Csci8802: Advanced Software Engineering.  University of Minnesota, Spring Semester 2015

SEng 5861: Software Architecture.  University of Minnesota, Fall Semester 2014, 2013, 2012, 2011, 2010

SEng 5841: Model-Based Software Development and Analysis.  University of Minnesota, Spring Semester 2007 

Professional Information

Miscellaneous Awards and Honors:

2016 Featured Faculty Member on the University of Minnesota “Driven To Discover” Campaign

2015 Dagstuhl Seminar Participant: Qualification of Formal Methods Tools

2014 Shonan Seminar Participant: Integration of Formal Methods and Testing for Model-Based Systems Engineering

2014 Inducted to IFIP 2.9 Working Group on Requirements

2013 MODELS Conference Best Reviewer Award

2012 Requirements Engineering Conference Ready-Set-Transfer contest winner

2012 Dagstuhl Seminar Participant: Architecture-Driven Semantic Analysis of Embedded Systems

2012 Senior Member IEEE
2010 Dagstuhl Seminar Participant: Practical Software Testing

Education/Academic qualification

PhD, University of Minnesota

Research interests

  • Model Checking
  • Software Testing
  • Requirements Engineering
  • Safety Critical Systems

Fingerprint The Fingerprint is created by mining the titles and abstracts of the person's research outputs and projects/funding awards to create an index of weighted terms from discipline-specific thesauri.

  • 2 Similar Profiles
Avionics Engineering & Materials Science
Specifications Engineering & Materials Science
Testing Engineering & Materials Science
Formal methods Engineering & Materials Science
Coverage Mathematics
Software engineering Engineering & Materials Science
Requirements Mathematics
Model checking Engineering & Materials Science

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Projects 2010 2021

Research Output 1997 2018

5 Citations (Scopus)

A Formal Approach to Constructing Secure Air Vehicle Software

Cofer, D., Gacek, A., Backes, J., Whalen, M. W., Pike, L., Foltzer, A., Podhradsky, M., Klein, G., Kuz, I., Andronick, J., Heiser, G. & Stuart, D., Nov 1 2018, Computer, 51, 11, p. 14-23 10 p.

Research output: Contribution to specialist publicationArticle

Formal methods

Ensuring the Observability of Structural Test Obligations

Meng, Y., Gay, G. & Whalen, M., Sep 5 2018, (Accepted/In press) In : IEEE Transactions on Software Engineering.

Research output: Contribution to journalArticle


Guest editorial: advanced topics in automated software engineering

Grunske, L. & Whalen, M., Dec 1 2018, In : Automated Software Engineering. 25, 4, p. 743-744 2 p.

Research output: Contribution to journalEditorial

Software engineering
1 Citation (Scopus)

Online enumeration of all minimal inductive validity cores

Bendík, J., Ghassabani, E., Whalen, M. & Černá, I., Jan 1 2018, Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Proceedings. Johnsen, E. B. & Schaefer, I. (eds.). Springer- Verlag, p. 189-204 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10886 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Robustness Analysis
Minimal Set
4 Citations (Scopus)

The JKind model checker

Gacek, A., Backes, J., Whalen, M., Wagner, L. & Ghassabani, E., Jan 1 2018, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Weissenbacher, G. & Chockler, H. (eds.). Springer- Verlag, p. 20-27 8 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10982 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
Industrial Application
Open Source
Industrial applications