Michael W. Whalen

Publication Activity (10 Years)

Years Active: 1991-2023
Publications (10 Years): 36

Top Topics

Test Case Generation

Top Venues

IEEE Trans. Software Eng.

Publications

Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. TACAS (1) (2023)
Soha Hussein, Qiuchen Yan, Stephen McCamant, Vaibhav Sharma, Michael W. Whalen
Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution). TACAS (2) (2023)
Benjamin Kiesl-Reiter, Michael W. Whalen
Proofs for Incremental SAT with Inprocessing. FMCAD (2023)
Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi, Vaibhav Sharma, Michael W. Whalen, Raveesh Yadav
Automated Analyses of IOT Event Monitoring Systems. CAV (1) (2023)
Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
Migrating Solver State. SAT (2022)
Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen
From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET. FM (2021)
Danielle Stewart, Jing Liu, Darren D. Cofer, Mats Per Erik Heimdahl, Michael W. Whalen, Michael Peterson
AADL-Based safety analysis using formal methods applied to aircraft digital systems. Reliab. Eng. Syst. Saf. 213 (2021)
Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek, Mats Per Erik Heimdahl
Inductive Validity Cores. IEEE Trans. Software Eng. 47 (2) (2021)
Danielle Stewart, Michael W. Whalen, Mats Per Erik Heimdahl, Jing Liu, Darren D. Cofer
Composition of Fault Forests. SAFECOMP (2021)
Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
Java Ranger at SV-COMP 2020 (Competition Contribution). TACAS (2) (2020)
Ying Meng, Gregory Gay, Michael W. Whalen
Ensuring the Observability of Structural Test Obligations. IEEE Trans. Software Eng. 46 (7) (2020)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. ASE (2020)
Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
Java Ranger: statically summarizing regions for efficient symbolic execution of Java. ESEC/SIGSOFT FSE (2020)
Judith Bishop, Kendra M. L. Cooper, Helen Sharp, Michael W. Whalen
Introduction to the special issue on software engineering in practice. Softw. Pract. Exp. 50 (3) (2020)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. CoRR (2020)
John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf, Cole Schlesinger, Rima Tanash, Carsten Varming, Michael W. Whalen
One-Click Formal Methods. IEEE Softw. 36 (6) (2019)
Darren D. Cofer, Andrew Gacek, John Backes, Michael W. Whalen, Lee Pike, Adam Foltzer, Michal Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser, Douglas Stuart
A Formal Approach to Constructing Secure Air Vehicle Software. Computer 51 (11) (2018)
Jaroslav Bendík, Elaheh Ghassabani, Michael W. Whalen, Ivana Cerná
Online Enumeration of All Minimal Inductive Validity Cores. SEFM (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR (2017)
Vaibhav Sharma, Michael W. Whalen, Stephen McCamant, Willem Visser
Veritesting Challenges in Symbolic Execution of Java. ACM SIGSOFT Softw. Eng. Notes 42 (4) (2017)
Danielle Stewart, Michael W. Whalen, Darren D. Cofer, Mats Per Erik Heimdahl
Architectural Modeling and Analysis for Safety Engineering. IMBSA (2017)
Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek
Efficient generation of all minimal inductive validity cores. FMCAD (2017)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Per Erik Heimdahl, Lucas G. Wagner
Proof-based coverage metrics for formal verification. ASE (2017)
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning About Algebraic Data Types with Abstractions. J. Autom. Reason. 57 (4) (2016)
John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
On Implementing Real-time Specification Patterns Using Observers. CoRR (2016)
Gregory Gay, Ajitha Rajan, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
The Effect of Program and Model Structure on the Effectiveness of MC/DC Test Adequacy Coverage. ACM Trans. Softw. Eng. Methodol. 25 (3) (2016)
Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR (2016)
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning about Algebraic Data Types with Abstractions. CoRR (2016)
Anitha Murugesan, Michael W. Whalen, Elaheh Ghassabani, Mats Per Erik Heimdahl
Complete Traceability for Requirements in Satisfaction Arguments. RE (2016)
Michael W. Whalen, Darren D. Cofer, Andrew Gacek
Requirements and Architectures for Secure Vehicles. IEEE Softw. 33 (4) (2016)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
Efficient Generation of Inductive Validity Cores for Safety Properties. CoRR (2016)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. FormaliSE@ICSE (2016)
Andreas Katis, Michael W. Whalen, Andrew Gacek
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report. CoRR (2016)
John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
On Implementing Real-Time Specification Patterns Using Observers. NFM (2016)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
Efficient generation of inductive validity cores for safety properties. SIGSOFT FSE (2016)
Anitha Murugesan, Michael W. Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Per Erik Heimdahl, Dongjiang You
Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites. NFM (2015)
Anitha Murugesan, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl
Design Considerations for Modeling Modes in Cyber-Physical Systems. IEEE Des. Test 32 (5) (2015)
John Backes, Darren D. Cofer, Steven P. Miller, Michael W. Whalen
Requirements Analysis of a Quad-Redundant Flight Control System. NFM (2015)
Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
The Risks of Coverage-Directed Test Case Generation. IEEE Trans. Software Eng. 41 (8) (2015)
Michael W. Whalen, Sanjai Rayadurgam, Elaheh Ghassabani, Anitha Murugesan, Oleg Sokolsky, Mats Per Erik Heimdahl, Insup Lee
Hierarchical multi-formalism proofs of cyber-physical systems. MEMOCODE (2015)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Machine-Checked Proofs For Realizability Checking Algorithms. CoRR (2015)
Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
Towards Realizability Checking of Contracts using Theories. CoRR (2015)
Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
Automated Oracle Data Selection Support. IEEE Trans. Software Eng. 41 (11) (2015)
Michael W. Whalen, Suzette Person, Neha Rungta, Matt Staats, Daniela Grijincu
A Flexible and Non-intrusive Approach for Computing Complex Structural Coverage Metrics. ICSE (1) (2015)
Dongjiang You, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl, Gregory Gay
Efficient observability-based test generation by dynamic symbolic execution. ISSRE (2015)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Machine-Checked Proofs for Realizability Checking Algorithms. VSTTE (2015)
Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
Towards Realizability Checking of Contracts Using Theories. NFM (2015)
Anitha Murugesan, Mats Per Erik Heimdahl, Michael W. Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, BaekGyu Kim, Oleg Sokolsky, Insup Lee
From Requirements to Code: Model Based Development of a Medical Cyber Physical System. FHIES/SEHC (2014)
Anitha Murugesan, Lu Feng, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael W. Whalen, Insup Lee
Exploring the twin peaks using probabilistic verification techniques. TwinPeaks (2014)
Michael W. Whalen, Anitha Murugesan, Sanjai Rayadurgam, Mats Per Erik Heimdahl
Structuring simulink models for verification and reuse. MiSE (2014)
Jason Biatek, Michael W. Whalen, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael R. Lowry
Analysis and testing of PLEXIL plans. FormaliSE (2014)
Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl, Insup Lee
Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. ICCPS (2014)
Neha Rungta, Oksana Tkachuk, Suzette Person, Jason Biatek, Michael W. Whalen, Joseph Castle, Karen Gundy-Burlet
Helping system engineers bridge the peaks. TwinPeaks (2014)
Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
Moving the goalposts: coverage satisfaction is not enough. SBST (2014)
Tuan-Hung Pham, Michael W. Whalen
An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. VSTTE (2013)
Michael W. Whalen, Andrew Gacek, Darren D. Cofer, Anitha Murugesan, Mats Per Erik Heimdahl, Sanjai Rayadurgam
Your "What" Is My "How": Iteration and Hierarchy in System Design. IEEE Softw. 30 (2) (2013)
Tuan-Hung Pham, Michael W. Whalen
RADA: a tool for reasoning about algebraic data types with abstractions. ESEC/SIGSOFT FSE (2013)
Michael W. Whalen
Up and out: scaling formal analysis using model-based development and architecture modeling. HILT (2013)
Anitha Murugesan, Michael W. Whalen, Sanjai Rayadurgam, Mats Per Erik Heimdahl
Compositional verification of a medical device system. HILT (2013)
Michael W. Whalen, Gregory Gay, Dongjiang You, Mats Per Erik Heimdahl, Matt Staats
Observable modified Condition/Decision coverage. ICSE (2013)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
A DSL for cross-domain security. HILT (2012)
Michael W. Whalen, Anitha Murugesan, Mats Per Erik Heimdahl
Your what is my how: Why requirements and architectural design should be iterative. TwinPeaks@RE (2012)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
The Guardol Language and Verification System. TACAS (2012)
Matt Staats, Gregory Gay, Michael W. Whalen, Mats Per Erik Heimdahl
On the Danger of Coverage Directed Test Case Generation. FASE (2012)
Daniel Balasubramanian, Corina S. Pasareanu, Jason Biatek, Thomas Pressburger, Gabor Karsai, Michael R. Lowry, Michael W. Whalen
Integrating Statechart Components in Polyglot. NASA Formal Methods (2012)
Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha
Compositional Verification of Architectural Models. NASA Formal Methods (2012)
Willem Visser, Matthew B. Dwyer, Michael W. Whalen
The hidden models of model checking. Softw. Syst. Model. 11 (4) (2012)
Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
Better testing through oracle selection. ICSE (2011)
Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
Programs, tests, and oracles: the foundations of testing revisited. ICSE (2011)
Daniel Balasubramanian, Corina S. Pasareanu, Michael W. Whalen, Gabor Karsai, Michael R. Lowry
Polyglot: modeling and analysis for multiple Statechart formalisms. ISSTA (2011)
Matt Staats, Michael W. Whalen, Ajitha Rajan, Mats Per Erik Heimdahl
Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness. NASA Formal Methods (2010)
Steven P. Miller, Michael W. Whalen, Darren D. Cofer
Software model checking takes off. Commun. ACM 53 (2) (2010)
Michael W. Whalen, Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser
FITE: future integrated testing environment. FoSER (2010)
Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, Michael W. Whalen
FITE - Future Integrated Testing Environment. Practical Software Testing: Tool Automation and Human Factors (2010)
David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen
Development of Security Software: A High Assurance Methodology. ICFEM (2009)
Darren D. Cofer, Michael W. Whalen, Steven P. Miller
Model-Checking of Safety-Critical Software for Avionics. ERCIM News 2008 (75) (2008)
Ajitha Rajan, Michael W. Whalen, Mats Per Erik Heimdahl
The effect of program and model structure on mc/dc test adequacy coverage. ICSE (2008)
Ajitha Rajan, Michael W. Whalen, Matt Staats, Mats Per Erik Heimdahl
Requirements Coverage as an Adequacy Measure for Conformance Testing. ICFEM (2008)
Ajitha Rajan, Michael W. Whalen, Mats Per Erik Heimdahl
Model Validation using Automatically Generated Requirements-Based Tests. HASE (2007)
Michael W. Whalen, Darren D. Cofer, Steven P. Miller, Bruce H. Krogh, Walter Storm
Integration of Formal Analysis into a Model-Based Software Development Process. FMICS (2007)
Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl
Proving the shalls. Int. J. Softw. Tools Technol. Transf. 8 (4-5) (2006)
Michael W. Whalen, Ajitha Rajan, Mats Per Erik Heimdahl, Steven P. Miller
Coverage metrics for requirements-based testing. ISSTA (2006)
Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen
Deviation Analysis: A New Use of Model Checking. Autom. Softw. Eng. 12 (3) (2005)
Johann Schumann, Bernd Fischer, Michael W. Whalen, Jon Whittle
Certification Support for Automatically Generated Programs. HICSS (2003)
Mats Per Erik Heimdahl, Michael W. Whalen, Jeffrey M. Thompson
NIMBUS: A Tool for Specification Centered Development. RE (2003)
Michael W. Whalen, Johann Schumann, Bernd Fischer
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. CADE (2002)
Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen
Deviation Analysis Through Model Checking. ASE (2002)
Michael W. Whalen, Johann Schumann, Bernd Fischer
Synthesizing Certified Code. FME (2002)
Michael W. Whalen
High-integrity code generation for state-based formalisms. ICSE (2000)
Jeffrey M. Thompson, Michael W. Whalen, Mats Per Erik Heimdahl
Requirements Capture and Evaluation in Nimbus: The Light-Control Case Study. J. Univers. Comput. Sci. 6 (7) (2000)
Michael W. Whalen, Mats Per Erik Heimdahl
An Approach to Automatic Code Generation for Safety-Critical Systems. ASE (1999)
Michael W. Whalen, Mats Per Erik Heimdahl
On the Requirements of High-Integrity Code Generation. HASE (1999)
Mats Per Erik Heimdahl, Jeffrey M. Thompson, Michael W. Whalen
On the Effectiveness of Slicing Hierarchical State Machines: A Case Study. EUROMICRO (1998)
Mats Per Erik Heimdahl, Michael W. Whalen
Reduction and Slicing of Hierarchical State Machines. ESEC / SIGSOFT FSE (1997)
Paul D. Gader, Michael W. Whalen, Margaret Ganzberger, Daniel J. Hepp
Handprinted word recognition on a NIST data set. Mach. Vis. Appl. 8 (1) (1995)
Paul D. Gader, Brian Forester, Margaret Ganzberger, Andrew M. Gillies, Brian T. Mitchell, Michael W. Whalen, Todd Yocum
Recognition of handwritten digits using template and model matching. Pattern Recognit. 24 (5) (1991)