Michael W. Whalen

Orcid: 0000-0003-3824-1435

Affiliations:
  • Amazon Web Services, USA
  • University of Minnesota, Minneapolis, USA (former)


According to our database1, Michael W. Whalen authored at least 96 papers between 1991 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.
CoRR, 2024

2023
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Proofs for Incremental SAT with Inprocessing.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

Automated Analyses of IOT Event Monitoring Systems.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Structural Test Input Generation for 3-Address Code Coverage Using Path-Merged Symbolic Execution.
Proceedings of the IEEE/ACM International Conference on Automation of Software Test, 2023

2022
Migrating Solver State.
Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

2021
Inductive Validity Cores.
IEEE Trans. Software Eng., 2021

AADL-Based safety analysis using formal methods applied to aircraft digital systems.
Reliab. Eng. Syst. Saf., 2021

Composition of Fault Forests.
Proceedings of the Computer Safety, Reliability, and Security, 2021

From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET.
Proceedings of the Formal Methods - 24th International Symposium, 2021

2020
Ensuring the Observability of Structural Test Obligations.
IEEE Trans. Software Eng., 2020

Introduction to the special issue on software engineering in practice.
Softw. Pract. Exp., 2020

Java Ranger at SV-COMP 2020 (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Java Ranger: statically summarizing regions for efficient symbolic execution of Java.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

Synthesis of Infinite-State Systems with Random Behavior.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

2019
One-Click Formal Methods.
IEEE Softw., 2019

2018
A Formal Approach to Constructing Secure Air Vehicle Software.
Computer, 2018

Guest editorial: advanced topics in automated software engineering.
Autom. Softw. Eng., 2018

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Online Enumeration of All Minimal Inductive Validity Cores.
Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

The JKind Model Checker.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Veritesting Challenges in Symbolic Execution of Java.
ACM SIGSOFT Softw. Eng. Notes, 2017

Proof-based coverage metrics for formal verification.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Architectural Modeling and Analysis for Safety Engineering.
Proceedings of the Model-Based Safety and Assessment - 5th International Symposium, 2017

Efficient generation of all minimal inductive validity cores.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016
The Effect of Program and Model Structure on the Effectiveness of MC/DC Test Adequacy Coverage.
ACM Trans. Softw. Eng. Methodol., 2016

Requirements and Architectures for Secure Vehicles.
IEEE Softw., 2016

Reasoning About Algebraic Data Types with Abstractions.
J. Autom. Reason., 2016

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability.
CoRR, 2016

Efficient generation of inductive validity cores for safety properties.
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Complete Traceability for Requirements in Satisfaction Arguments.
Proceedings of the 24th IEEE International Requirements Engineering Conference, 2016

On Implementing Real-Time Specification Patterns Using Observers.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report.
Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, 2016

2015
Automated Oracle Data Selection Support.
IEEE Trans. Software Eng., 2015

The Risks of Coverage-Directed Test Case Generation.
IEEE Trans. Software Eng., 2015

Design Considerations for Modeling Modes in Cyber-Physical Systems.
IEEE Des. Test, 2015

Machine-Checked Proofs for Realizability Checking Algorithms.
Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Towards Realizability Checking of Contracts Using Theories.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Requirements Analysis of a Quad-Redundant Flight Control System.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Hierarchical multi-formalism proofs of cyber-physical systems.
Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

Efficient observability-based test generation by dynamic symbolic execution.
Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering, 2015

A Flexible and Non-intrusive Approach for Computing Complex Structural Coverage Metrics.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

2014
Resolute: an assurance case language for architecture models.
Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

Structuring simulink models for verification and reuse.
Proceedings of the 6th International Workshop on Modeling in Software Engineering, 2014

Helping system engineers bridge the peaks.
Proceedings of the 4th International Workshop on Twin Peaks of Requirements and Architecture, 2014

Exploring the twin peaks using probabilistic verification techniques.
Proceedings of the 4th International Workshop on Twin Peaks of Requirements and Architecture, 2014

Moving the goalposts: coverage satisfaction is not enough.
Proceedings of the 7th International Workshop on Search-Based Software Testing, 2014

Analysis and testing of PLEXIL plans.
Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering, 2014

Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety.
Proceedings of the ACM/IEEE International Conference on Cyber-Physical Systems, 2014

From Requirements to Code: Model Based Development of a Medical Cyber Physical System.
Proceedings of the Software Engineering in Health Care - 4th International Symposium, 2014

2013
Your "What" Is My "How": Iteration and Hierarchy in System Design.
IEEE Softw., 2013

An Improved Unrolling-Based Decision Procedure for Algebraic Data Types.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

RADA: a tool for reasoning about algebraic data types with abstractions.
Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Up and out: scaling formal analysis using model-based development and architecture modeling.
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

Compositional verification of a medical device system.
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

Observable modified Condition/Decision coverage.
Proceedings of the 35th International Conference on Software Engineering, 2013

2012
The hidden models of model checking.
Softw. Syst. Model., 2012

The Guardol Language and Verification System.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

A DSL for cross-domain security.
Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

Your what is my how: Why requirements and architectural design should be iterative.
Proceedings of the First IEEEInternational Workshop on the Twin Peaks of Requirements and Architecture, 2012

Incremental Verification with Mode Variable Invariants in State Machines.
Proceedings of the NASA Formal Methods, 2012

Compositional Verification of Architectural Models.
Proceedings of the NASA Formal Methods, 2012

Integrating Statechart Components in Polyglot.
Proceedings of the NASA Formal Methods, 2012

On the Danger of Coverage Directed Test Case Generation.
Proceedings of the Fundamental Approaches to Software Engineering, 2012

2011
Polyglot: modeling and analysis for multiple Statechart formalisms.
Proceedings of the 20th International Symposium on Software Testing and Analysis, 2011

Better testing through oracle selection.
Proceedings of the 33rd International Conference on Software Engineering, 2011

Programs, tests, and oracles: the foundations of testing revisited.
Proceedings of the 33rd International Conference on Software Engineering, 2011

2010
Software model checking takes off.
Commun. ACM, 2010

Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness.
Proceedings of the Second NASA Formal Methods Symposium, 2010

FITE - Future Integrated Testing Environment.
Proceedings of the Practical Software Testing: Tool Automation and Human Factors, 14.03., 2010

Model Checking Information Flow.
Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009
Development of Security Software: A High Assurance Methodology.
Proceedings of the Formal Methods and Software Engineering, 2009

2008
Model-Checking of Safety-Critical Software for Avionics.
ERCIM News, 2008

The effect of program and model structure on mc/dc test adequacy coverage.
Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

Requirements Coverage as an Adequacy Measure for Conformance Testing.
Proceedings of the Formal Methods and Software Engineering, 2008

2007
Extending Lustre with Timeout Automata.
Proceedings of the International Workshop on Model-driven High-level Programming of Embedded Systems, 2007

Model Validation using Automatically Generated Requirements-Based Tests.
Proceedings of the Tenth IEEE International Symposium on High Assurance Systems Engineering (HASE 2007), 2007

Integration of Formal Analysis into a Model-Based Software Development Process.
Proceedings of the Formal Methods for Industrial Critical Systems, 2007

2006
Proving the shalls.
Int. J. Softw. Tools Technol. Transf., 2006

Coverage metrics for requirements-based testing.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2006

2005
Deviation Analysis: A New Use of Model Checking.
Autom. Softw. Eng., 2005

2003
NIMBUS: A Tool for Specification Centered Development.
Proceedings of the 11th IEEE International Conference on Requirements Engineering (RE 2003), 2003

Certification Support for Automatically Generated Programs.
Proceedings of the 36th Hawaii International Conference on System Sciences (HICSS-36 2003), 2003

2002
Deviation Analysis Through Model Checking.
Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 2002

Synthesizing Certified Code.
Proceedings of the FME 2002: Formal Methods, 2002

AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description.
Proceedings of the Automated Deduction, 2002

2000
Requirements Capture and Evaluation in Nimbus: The Light-Control Case Study.
J. Univers. Comput. Sci., 2000

High-integrity code generation for state-based formalisms.
Proceedings of the 22nd International Conference on on Software Engineering, 2000

1999
An Approach to Automatic Code Generation for Safety-Critical Systems.
Proceedings of the 14th IEEE International Conference on Automated Software Engineering, 1999

On the Requirements of High-Integrity Code Generation.
Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE '99), 1999

1998
On the Effectiveness of Slicing Hierarchical State Machines: A Case Study.
Proceedings of the 24th EUROMICRO '98 Conference, 1998

1997
Reduction and Slicing of Hierarchical State Machines.
Proceedings of the Software Engineering, 1997

1995
Handprinted word recognition on a NIST data set.
Mach. Vis. Appl., 1995

1991
Recognition of handwritten digits using template and model matching.
Pattern Recognit., 1991


  Loading...