Recognition of handwritten digits using template and model matching. - Paul D. Gader; Brian Forester; Margaret Ganzberger; Andrew M. Gillies; Brian T. Mitchell; Michael W. Whalen; Todd Yocum (Pattern Recognit., 1991)

Handprinted word recognition on a NIST data set. - Paul D. Gader; Michael W. Whalen; Margaret Ganzberger; Daniel J. Hepp (Mach. Vis. Appl., 1995)

Reduction and Slicing of Hierarchical State Machines. - Mats Per Erik Heimdahl; Michael W. Whalen (ESEC / SIGSOFT FSE, 1997)

On the Effectiveness of Slicing Hierarchical State Machines: A Case Study. - Mats Per Erik Heimdahl; Jeffrey M. Thompson; Michael W. Whalen (EUROMICRO, 1998)

On the Requirements of High-Integrity Code Generation. - Michael W. Whalen; Mats Per Erik Heimdahl (HASE, 1999)

An Approach to Automatic Code Generation for Safety-Critical Systems. - Michael W. Whalen; Mats Per Erik Heimdahl (ASE, 1999)

High-integrity code generation for state-based formalisms. - Michael W. Whalen (ICSE, 2000)

Requirements Capture and Evaluation in Nimbus: The Light-Control Case Study. - Jeffrey M. Thompson; Michael W. Whalen; Mats Per Erik Heimdahl (J. Univers. Comput. Sci., 2000)

AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. - Michael W. Whalen; Johann Schumann; Bernd Fischer 002 (CADE, 2002)

Synthesizing Certified Code. - Michael W. Whalen; Johann Schumann; Bernd Fischer 002 (FME, 2002)

Deviation Analysis Through Model Checking. - Mats Per Erik Heimdahl; Yunja Choi; Michael W. Whalen (ASE, 2002)

Certification Support for Automatically Generated Programs. - Johann Schumann; Bernd Fischer 002; Michael W. Whalen; Jon Whittle 001 (HICSS, 2003)

NIMBUS: A Tool for Specification Centered Development. - Mats Per Erik Heimdahl; Michael W. Whalen; Jeffrey M. Thompson (RE, 2003)

Deviation Analysis: A New Use of Model Checking. - Mats Per Erik Heimdahl; Yunja Choi; Michael W. Whalen (Autom. Softw. Eng., 2005)

Coverage metrics for requirements-based testing. - Michael W. Whalen; Ajitha Rajan; Mats Per Erik Heimdahl; Steven P. Miller (ISSTA, 2006)

Proving the shalls. - Steven P. Miller; Alan C. Tribble; Michael W. Whalen; Mats Per Erik Heimdahl (Int. J. Softw. Tools Technol. Transf., 2006)

Integration of Formal Analysis into a Model-Based Software Development Process. - Michael W. Whalen; Darren D. Cofer; Steven P. Miller; Bruce H. Krogh; Walter Storm (FMICS, 2007)

Model Validation using Automatically Generated Requirements-Based Tests. - Ajitha Rajan; Michael W. Whalen; Mats Per Erik Heimdahl (HASE, 2007)

Extending Lustre with Timeout Automata. - Jimin Gao; Mike Whalen; Eric Van Wyk (SLA++P@ETAPS, 2007)

Requirements Coverage as an Adequacy Measure for Conformance Testing. - Ajitha Rajan; Michael W. Whalen; Matt Staats; Mats Per Erik Heimdahl (ICFEM, 2008)

The effect of program and model structure on mc/dc test adequacy coverage. - Ajitha Rajan; Michael W. Whalen; Mats Per Erik Heimdahl (ICSE, 2008)

Model-Checking of Safety-Critical Software for Avionics. - Darren D. Cofer; Michael W. Whalen; Steven P. Miller (ERCIM News, 2008)

Development of Security Software: A High Assurance Methodology. - David S. Hardin; T. Douglas Hiratzka; D. Randolph Johnson; Lucas G. Wagner; Michael W. Whalen (ICFEM, 2009)

Model Checking Information Flow. - Michael W. Whalen; David A. Greve; Lucas G. Wagner (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness. - Matt Staats; Michael W. Whalen; Ajitha Rajan; Mats Per Erik Heimdahl (NASA Formal Methods, 2010)

FITE: future integrated testing environment. - Michael W. Whalen; Patrice Godefroid; Leonardo Mariani; Andrea Polini; Nikolai Tillmann; Willem Visser (FoSER, 2010)

Software model checking takes off. - Steven P. Miller; Michael W. Whalen; Darren D. Cofer (Commun. ACM, 2010)

Programs, tests, and oracles: the foundations of testing revisited. - Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (ICSE, 2011)

Better testing through oracle selection. - Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (ICSE, 2011)

Polyglot: modeling and analysis for multiple Statechart formalisms. - Daniel Balasubramanian; Corina S. Pasareanu; Michael W. Whalen; Gabor Karsai; Michael R. Lowry (ISSTA, 2011)

On the Danger of Coverage Directed Test Case Generation. - Matt Staats; Gregory Gay 002; Michael W. Whalen; Mats Per Erik Heimdahl (FASE, 2012)

Integrating Statechart Components in Polyglot. - Daniel Balasubramanian; Corina S. Pasareanu; Jason Biatek; Thomas Pressburger; Gabor Karsai; Michael R. Lowry; Michael W. Whalen (NASA Formal Methods, 2012)

Compositional Verification of Architectural Models. - Darren D. Cofer; Andrew Gacek; Steven P. Miller; Michael W. Whalen; Brian LaValley; Lui Sha (NASA Formal Methods, 2012)

Incremental Verification with Mode Variable Invariants in State Machines. - Temesghen Kahsai; Pierre-Loïc Garoche; Cesare Tinelli; Mike Whalen (NASA Formal Methods, 2012)

Your what is my how: Why requirements and architectural design should be iterative. - Michael W. Whalen; Anitha Murugesan; Mats Per Erik Heimdahl (TwinPeaks@RE, 2012)

A DSL for cross-domain security. - David S. Hardin; Konrad Slind; Michael W. Whalen; Tuan-Hung Pham (HILT, 2012)

The Guardol Language and Verification System. - David S. Hardin; Konrad Slind; Michael W. Whalen; Tuan-Hung Pham (TACAS, 2012)

The hidden models of model checking. - Willem Visser; Matthew B. Dwyer; Michael W. Whalen (Softw. Syst. Model., 2012)

Observable modified Condition/Decision coverage. - Michael W. Whalen; Gregory Gay 002; Dongjiang You; Mats Per Erik Heimdahl; Matt Staats (ICSE, 2013)

Compositional verification of a medical device system. - Anitha Murugesan; Michael W. Whalen; Sanjai Rayadurgam; Mats Per Erik Heimdahl (HILT, 2013)

Up and out: scaling formal analysis using model-based development and architecture modeling. - Michael W. Whalen (HILT, 2013)

RADA: a tool for reasoning about algebraic data types with abstractions. - Tuan-Hung Pham; Michael W. Whalen (ESEC/SIGSOFT FSE, 2013)

An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. - Tuan-Hung Pham; Michael W. Whalen (VSTTE, 2013)

Your "What" Is My "How": Iteration and Hierarchy in System Design. - Michael W. Whalen; Andrew Gacek; Darren D. Cofer; Anitha Murugesan; Mats Per Erik Heimdahl; Sanjai Rayadurgam (IEEE Softw., 2013)

From Requirements to Code: Model Based Development of a Medical Cyber Physical System. - Anitha Murugesan; Mats Per Erik Heimdahl; Michael W. Whalen; Sanjai Rayadurgam; John Komp; Lian Duan; BaekGyu Kim; Oleg Sokolsky; Insup Lee 001 (FHIES/SEHC, 2014)

Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. - Anitha Murugesan; Oleg Sokolsky; Sanjai Rayadurgam; Michael W. Whalen; Mats Per Erik Heimdahl; Insup Lee 001 (ICCPS, 2014)

Analysis and testing of PLEXIL plans. - Jason Biatek; Michael W. Whalen; Mats Per Erik Heimdahl; Sanjai Rayadurgam; Michael R. Lowry (FormaliSE, 2014)

Moving the goalposts: coverage satisfaction is not enough. - Gregory Gay 002; Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (SBST, 2014)

Exploring the twin peaks using probabilistic verification techniques. - Anitha Murugesan; Lu Feng 001; Mats Per Erik Heimdahl; Sanjai Rayadurgam; Michael W. Whalen; Insup Lee 001 (TwinPeaks, 2014)

Helping system engineers bridge the peaks. - Neha Rungta; Oksana Tkachuk; Suzette Person; Jason Biatek; Michael W. Whalen; Joseph Castle; Karen Gundy-Burlet (TwinPeaks, 2014)

Structuring simulink models for verification and reuse. - Michael W. Whalen; Anitha Murugesan; Sanjai Rayadurgam; Mats Per Erik Heimdahl (MiSE, 2014)

Resolute: an assurance case language for architecture models. - Andrew Gacek; John Backes; Darren D. Cofer; Konrad Slind; Mike Whalen (HILT, 2014)

A Flexible and Non-intrusive Approach for Computing Complex Structural Coverage Metrics. - Michael W. Whalen; Suzette Person; Neha Rungta; Matt Staats; Daniela Grijincu (ICSE (1), 2015)

Efficient observability-based test generation by dynamic symbolic execution. - Dongjiang You; Sanjai Rayadurgam; Michael W. Whalen; Mats Per Erik Heimdahl; Gregory Gay 002 (ISSRE, 2015)

Hierarchical multi-formalism proofs of cyber-physical systems. - Michael W. Whalen; Sanjai Rayadurgam; Elaheh Ghassabani; Anitha Murugesan; Oleg Sokolsky; Mats Per Erik Heimdahl; Insup Lee 001 (MEMOCODE, 2015)

Requirements Analysis of a Quad-Redundant Flight Control System. - John Backes; Darren D. Cofer; Steven P. Miller; Michael W. Whalen (NFM, 2015)

Towards Realizability Checking of Contracts Using Theories. - Andrew Gacek; Andreas Katis; Michael W. Whalen; John Backes; Darren D. Cofer (NFM, 2015)

Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites. - Anitha Murugesan; Michael W. Whalen; Neha Rungta; Oksana Tkachuk; Suzette Person; Mats Per Erik Heimdahl; Dongjiang You (NFM, 2015)

Machine-Checked Proofs for Realizability Checking Algorithms. - Andreas Katis; Andrew Gacek; Michael W. Whalen (VSTTE, 2015)

Design Considerations for Modeling Modes in Cyber-Physical Systems. - Anitha Murugesan; Sanjai Rayadurgam; Michael W. Whalen; Mats Per Erik Heimdahl (IEEE Des. Test, 2015)

The Risks of Coverage-Directed Test Case Generation. - Gregory Gay 002; Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (IEEE Trans. Software Eng., 2015)

Automated Oracle Data Selection Support. - Gregory Gay 002; Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (IEEE Trans. Software Eng., 2015)

Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. - Andreas Katis; Andrew Gacek; Michael W. Whalen (FormaliSE@ICSE, 2016)

On Implementing Real-Time Specification Patterns Using Observers. - John D. Backes; Michael W. Whalen; Andrew Gacek; John Komp (NFM, 2016)

Complete Traceability for Requirements in Satisfaction Arguments. - Anitha Murugesan; Michael W. Whalen; Elaheh Ghassabani; Mats Per Erik Heimdahl (RE, 2016)

Efficient generation of inductive validity cores for safety properties. - Elaheh Ghassabani; Andrew Gacek; Michael W. Whalen (SIGSOFT FSE, 2016)

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. - Andreas Katis; Grigory Fedyukovich; Andrew Gacek; John D. Backes; Arie Gurfinkel; Michael W. Whalen (CoRR, 2016)

Reasoning About Algebraic Data Types with Abstractions. - Tuan-Hung Pham; Andrew Gacek; Michael W. Whalen (J. Autom. Reason., 2016)

Requirements and Architectures for Secure Vehicles. - Michael W. Whalen; Darren D. Cofer; Andrew Gacek (IEEE Softw., 2016)

The Effect of Program and Model Structure on the Effectiveness of MC/DC Test Adequacy Coverage. - Gregory Gay 002; Ajitha Rajan; Matt Staats; Michael W. Whalen; Mats Per Erik Heimdahl (ACM Trans. Softw. Eng. Methodol., 2016)

Efficient generation of all minimal inductive validity cores. - Elaheh Ghassabani; Michael W. Whalen; Andrew Gacek (FMCAD, 2017)

Architectural Modeling and Analysis for Safety Engineering. - Danielle Stewart; Michael W. Whalen; Darren D. Cofer; Mats Per Erik Heimdahl (IMBSA, 2017)

Proof-based coverage metrics for formal verification. - Elaheh Ghassabani; Andrew Gacek; Michael W. Whalen; Mats Per Erik Heimdahl; Lucas G. Wagner (ASE, 2017)

Veritesting Challenges in Symbolic Execution of Java. - Vaibhav Sharma 001; Michael W. Whalen; Stephen McCamant; Willem Visser (ACM SIGSOFT Softw. Eng. Notes, 2017)

The JKind Model Checker. - Andrew Gacek; John Backes; Mike Whalen; Lucas G. Wagner; Elaheh Ghassabani (CAV (2), 2018)

Online Enumeration of All Minimal Inductive Validity Cores. - Jaroslav Bendík; Elaheh Ghassabani; Michael W. Whalen; Ivana Cerná (SEFM, 2018)

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. - Andreas Katis; Grigory Fedyukovich; Huajun Guo; Andrew Gacek; John Backes; Arie Gurfinkel; Michael W. Whalen (TACAS (2), 2018)

Guest editorial: advanced topics in automated software engineering. - Lars Grunske; Mike Whalen (Autom. Softw. Eng., 2018)

A Formal Approach to Constructing Secure Air Vehicle Software. - 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 (Computer, 2018)

One-Click Formal Methods. - 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 (IEEE Softw., 2019)

Synthesis of Infinite-State Systems with Random Behavior. - Andreas Katis; Grigory Fedyukovich; Jeffrey Chen; David A. Greve; Sanjai Rayadurgam; Michael W. Whalen (ASE, 2020)

Java Ranger: statically summarizing regions for efficient symbolic execution of Java. - Vaibhav Sharma 001; Soha Hussein; Michael W. Whalen; Stephen McCamant; Willem Visser (ESEC/SIGSOFT FSE, 2020)

Java Ranger at SV-COMP 2020 (Competition Contribution). - Vaibhav Sharma 001; Soha Hussein; Michael W. Whalen; Stephen McCamant; Willem Visser (TACAS (2), 2020)

Introduction to the special issue on software engineering in practice. - Judith Bishop; Kendra M. L. Cooper; Helen Sharp; Michael W. Whalen (Softw. Pract. Exp., 2020)

Ensuring the Observability of Structural Test Obligations. - Ying Meng; Gregory Gay 002; Michael W. Whalen (IEEE Trans. Software Eng., 2020)

From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET. - Anastasia Mavridou; Andreas Katis; Dimitra Giannakopoulou; David Kooi; Thomas Pressburger; Michael W. Whalen (FM, 2021)

Composition of Fault Forests. - Danielle Stewart; Michael W. Whalen; Mats Per Erik Heimdahl; Jing Liu; Darren D. Cofer (SAFECOMP, 2021)

AADL-Based safety analysis using formal methods applied to aircraft digital systems. - Danielle Stewart; Jing Liu; Darren D. Cofer; Mats Per Erik Heimdahl; Michael W. Whalen; Michael Peterson (Reliab. Eng. Syst. Saf., 2021)

Inductive Validity Cores. - Elaheh Ghassabani; Michael W. Whalen; Andrew Gacek; Mats Per Erik Heimdahl (IEEE Trans. Software Eng., 2021)

Migrating Solver State. - Armin Biere; Md. Solimul Chowdhury; Marijn J. H. Heule; Benjamin Kiesl; Michael W. Whalen (SAT, 2022)

Structural Test Input Generation for 3-Address Code Coverage Using Path-Merged Symbolic Execution. - Soha Hussein; Stephen McCamant; Elena Sherman; Vaibhav Sharma 001; Mike Whalen (AST, 2023)

Automated Analyses of IOT Event Monitoring Systems. - Andrew Apicelli; Sam Bayless; Ankush Das; Andrew Gacek; Dhiva Jaganathan; Saswat Padhi; Vaibhav Sharma 001; Michael W. Whalen; Raveesh Yadav (CAV (1), 2023)

Proofs for Incremental SAT with Inprocessing. - Benjamin Kiesl-Reiter; Michael W. Whalen (FMCAD, 2023)

Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution). - Soha Hussein; Qiuchen Yan; Stephen McCamant; Vaibhav Sharma 001; Michael W. Whalen (TACAS (2), 2023)

Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. - Dawn Michaelson; Dominik Schreiber 001; Marijn J. H. Heule; Benjamin Kiesl-Reiter; Michael W. Whalen (TACAS (1), 2023)

SMT-D: New Strategies for Portfolio-Based SMT Solving. - Clark W. Barrett; Pei-Wei Chen; Byron Cook; Bruno Dutertre; Robert B. Jones; Nham Le; Andrew Reynolds 001; Kunal Sheth; Christopher Stephens; Michael W. Whalen (FMCAD, 2024)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories. - Nick Feng; Alan J. Hu; Sam Bayless; Syed M. Iqbal; Patrick Trentin; Mike Whalen; Lee Pike; John Backes (TACAS (1), 2024)

Generator-Based Fuzzers with Type-Based Targeted Mutation. - Soha Hussein; Stephen McCamant; Mike Whalen (CoRR, 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)

Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. - Dawn Michaelson; Dominik Schreiber 001; Marijn J. H. Heule; Benjamin Kiesl-Reiter; Michael W. Whalen (J. Autom. Reason., 2025)