Michael W. Whalen

102 papers A* 10A 8B 7C 5Journal 33Unranked 38

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A Neurosymbolic Approach to Natural Language Formalization and Verification. CoRR Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Marc Hudak, Dejan Jovanovic, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamaric, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao
2025	A*	`conf`	Formally Verified Cloud-Scale Authorization. ICSE Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2025	J	`jnl`	Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. J. Autom. Reason. Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
2024	B	`conf`	SMT-D: New Strategies for Portfolio-Based SMT Solving. FMCAD Clark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Christopher Stephens, Michael W. Whalen
2023	—	`conf`	Automated Analyses of IOT Event Monitoring Systems. CAV (1) Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi, Vaibhav Sharma, Michael W. Whalen, Raveesh Yadav
2023	—	`conf`	Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution). TACAS (2) Soha Hussein, Qiuchen Yan, Stephen McCamant, Vaibhav Sharma, Michael W. Whalen
2023	B	`conf`	Proofs for Incremental SAT with Inprocessing. FMCAD Benjamin Kiesl-Reiter, Michael W. Whalen
2023	—	`conf`	Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. TACAS (1) Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
2022	A	`conf`	Migrating Solver State. SAT Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
2021	J	`jnl`	AADL-Based safety analysis using formal methods applied to aircraft digital systems. Reliab. Eng. Syst. Saf. Danielle Stewart, Jing Liu, Darren D. Cofer, Mats Per Erik Heimdahl, Michael W. Whalen, Michael Peterson
2021	B	`conf`	Composition of Fault Forests. SAFECOMP Danielle Stewart, Michael W. Whalen, Mats Per Erik Heimdahl, Jing Liu, Darren D. Cofer
2021	B	`conf`	From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET. FM Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen
2021	J	`jnl`	Inductive Validity Cores. IEEE Trans. Software Eng. Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek, Mats Per Erik Heimdahl
2020	J	`jnl`	Ensuring the Observability of Structural Test Obligations. IEEE Trans. Software Eng. Ying Meng, Gregory Gay, Michael W. Whalen
2020	J	`jnl`	Introduction to the special issue on software engineering in practice. Softw. Pract. Exp. Judith Bishop, Kendra M. L. Cooper, Helen Sharp, Michael W. Whalen
2020	—	`conf`	Java Ranger at SV-COMP 2020 (Competition Contribution). TACAS (2) Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
2020	—	`conf`	Java Ranger: statically summarizing regions for efficient symbolic execution of Java. ESEC/SIGSOFT FSE Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
2020	A*	`conf`	Synthesis of Infinite-State Systems with Random Behavior. ASE Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
2020	J	`jnl`	Synthesis of Infinite-State Systems with Random Behavior. CoRR Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
2019	J	`jnl`	One-Click Formal Methods. IEEE Softw. John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf, Cole Schlesinger, Rima S. Tanash, Carsten Varming, Michael W. Whalen
2018	J	`jnl`	A Formal Approach to Constructing Secure Air Vehicle Software. Computer 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
2018	B	`conf`	Online Enumeration of All Minimal Inductive Validity Cores. SEFM Jaroslav Bendík, Elaheh Ghassabani, Michael W. Whalen, Ivana Cerná
2018	—	`conf`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
2017	—	`conf`	Architectural Modeling and Analysis for Safety Engineering. IMBSA Danielle Stewart, Michael W. Whalen, Darren D. Cofer, Mats Per Erik Heimdahl
2017	B	`conf`	Efficient generation of all minimal inductive validity cores. FMCAD Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek
2017	A*	`conf`	Proof-based coverage metrics for formal verification. ASE Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Per Erik Heimdahl, Lucas G. Wagner
2017	J	`jnl`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
2017	J	`jnl`	Veritesting Challenges in Symbolic Execution of Java. ACM SIGSOFT Softw. Eng. Notes Vaibhav Sharma, Michael W. Whalen, Stephen McCamant, Willem Visser
2016	A	`conf`	Complete Traceability for Requirements in Satisfaction Arguments. RE Anitha Murugesan, Michael W. Whalen, Elaheh Ghassabani, Mats Per Erik Heimdahl
2016	J	`jnl`	Efficient Generation of Inductive Validity Cores for Safety Properties. CoRR Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
2016	—	`conf`	Efficient generation of inductive validity cores for safety properties. SIGSOFT FSE Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
2016	—	`conf`	On Implementing Real-Time Specification Patterns Using Observers. NFM John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
2016	J	`jnl`	On Implementing Real-time Specification Patterns Using Observers. CoRR John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
2016	J	`jnl`	Reasoning About Algebraic Data Types with Abstractions. J. Autom. Reason. Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
2016	J	`jnl`	Reasoning about Algebraic Data Types with Abstractions. CoRR Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
2016	J	`jnl`	Requirements and Architectures for Secure Vehicles. IEEE Softw. Michael W. Whalen, Darren D. Cofer, Andrew Gacek
2016	J	`jnl`	Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
2016	J	`jnl`	The Effect of Program and Model Structure on the Effectiveness of MC/DC Test Adequacy Coverage. ACM Trans. Softw. Eng. Methodol. Gregory Gay, Ajitha Rajan, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2016	J	`jnl`	Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report. CoRR Andreas Katis, Michael W. Whalen, Andrew Gacek
2016	—	`conf`	Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. FormaliSE@ICSE Andreas Katis, Andrew Gacek, Michael W. Whalen
2015	—	`conf`	A Flexible and Non-intrusive Approach for Computing Complex Structural Coverage Metrics. ICSE (1) Michael W. Whalen, Suzette Person, Neha Rungta, Matt Staats, Daniela Grijincu
2015	—	`conf`	Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites. NFM Anitha Murugesan, Michael W. Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Per Erik Heimdahl, Dongjiang You
2015	J	`jnl`	Automated Oracle Data Selection Support. IEEE Trans. Software Eng. Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2015	J	`jnl`	Design Considerations for Modeling Modes in Cyber-Physical Systems. IEEE Des. Test Anitha Murugesan, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl
2015	A	`conf`	Efficient observability-based test generation by dynamic symbolic execution. ISSRE Dongjiang You, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl, Gregory Gay
2015	C	`conf`	Hierarchical multi-formalism proofs of cyber-physical systems. MEMOCODE Michael W. Whalen, Sanjai Rayadurgam, Elaheh Ghassabani, Anitha Murugesan, Oleg Sokolsky, Mats Per Erik Heimdahl, Insup Lee
2015	J	`jnl`	Machine-Checked Proofs For Realizability Checking Algorithms. CoRR Andreas Katis, Andrew Gacek, Michael W. Whalen
2015	—	`conf`	Machine-Checked Proofs for Realizability Checking Algorithms. VSTTE Andreas Katis, Andrew Gacek, Michael W. Whalen
2015	—	`conf`	Requirements Analysis of a Quad-Redundant Flight Control System. NFM John Backes, Darren D. Cofer, Steven P. Miller, Michael W. Whalen
2015	J	`jnl`	The Risks of Coverage-Directed Test Case Generation. IEEE Trans. Software Eng. Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2015	—	`conf`	Towards Realizability Checking of Contracts Using Theories. NFM Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
2015	J	`jnl`	Towards Realizability Checking of Contracts using Theories. CoRR Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
2014	—	`conf`	Analysis and testing of PLEXIL plans. FormaliSE Jason Biatek, Michael W. Whalen, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael R. Lowry
2014	—	`conf`	Exploring the twin peaks using probabilistic verification techniques. TwinPeaks Anitha Murugesan, Lu Feng, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael W. Whalen, Insup Lee
2014	—	`conf`	From Requirements to Code: Model Based Development of a Medical Cyber Physical System. FHIES/SEHC Anitha Murugesan, Mats Per Erik Heimdahl, Michael W. Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, BaekGyu Kim, Oleg Sokolsky, Insup Lee
2014	—	`conf`	Helping system engineers bridge the peaks. TwinPeaks Neha Rungta, Oksana Tkachuk, Suzette Person, Jason Biatek, Michael W. Whalen, Joseph Castle, Karen Gundy-Burlet
2014	—	`conf`	Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. ICCPS Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael W. Whalen, Mats Per Erik Heimdahl, Insup Lee
2014	—	`conf`	Moving the goalposts: coverage satisfaction is not enough. SBST Gregory Gay, Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2014	C	`conf`	Structuring simulink models for verification and reuse. MiSE Michael W. Whalen, Anitha Murugesan, Sanjai Rayadurgam, Mats Per Erik Heimdahl
2013	—	`conf`	An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. VSTTE Tuan-Hung Pham, Michael W. Whalen
2013	—	`conf`	Compositional verification of a medical device system. HILT Anitha Murugesan, Michael W. Whalen, Sanjai Rayadurgam, Mats Per Erik Heimdahl
2013	A*	`conf`	Observable modified Condition/Decision coverage. ICSE Michael W. Whalen, Gregory Gay, Dongjiang You, Mats Per Erik Heimdahl, Matt Staats
2013	—	`conf`	RADA: a tool for reasoning about algebraic data types with abstractions. ESEC/SIGSOFT FSE Tuan-Hung Pham, Michael W. Whalen
2013	—	`conf`	Up and out: scaling formal analysis using model-based development and architecture modeling. HILT Michael W. Whalen
2013	J	`jnl`	Your "What" Is My "How": Iteration and Hierarchy in System Design. IEEE Softw. Michael W. Whalen, Andrew Gacek, Darren D. Cofer, Anitha Murugesan, Mats Per Erik Heimdahl, Sanjai Rayadurgam
2012	—	`conf`	A DSL for cross-domain security. HILT David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
2012	—	`conf`	Compositional Verification of Architectural Models. NASA Formal Methods Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha
2012	—	`conf`	Integrating Statechart Components in Polyglot. NASA Formal Methods Daniel Balasubramanian, Corina S. Pasareanu, Jason Biatek, Thomas Pressburger, Gabor Karsai, Michael R. Lowry, Michael W. Whalen
2012	B	`conf`	On the Danger of Coverage Directed Test Case Generation. FASE Matt Staats, Gregory Gay, Michael W. Whalen, Mats Per Erik Heimdahl
2012	A	`conf`	The Guardol Language and Verification System. TACAS David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
2012	J	`jnl`	The hidden models of model checking. Softw. Syst. Model. Willem Visser, Matthew B. Dwyer, Michael W. Whalen
2012	—	`conf`	Your what is my how: Why requirements and architectural design should be iterative. TwinPeaks@RE Michael W. Whalen, Anitha Murugesan, Mats Per Erik Heimdahl
2011	A*	`conf`	Better testing through oracle selection. ICSE Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2011	A	`conf`	Polyglot: modeling and analysis for multiple Statechart formalisms. ISSTA Daniel Balasubramanian, Corina S. Pasareanu, Michael W. Whalen, Gabor Karsai, Michael R. Lowry
2011	A*	`conf`	Programs, tests, and oracles: the foundations of testing revisited. ICSE Matt Staats, Michael W. Whalen, Mats Per Erik Heimdahl
2010	—	`conf`	Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness. NASA Formal Methods Matt Staats, Michael W. Whalen, Ajitha Rajan, Mats Per Erik Heimdahl
2010	—	`conf`	FITE - Future Integrated Testing Environment. Practical Software Testing: Tool Automation and Human Factors Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, Michael W. Whalen
2010	—	`conf`	FITE: future integrated testing environment. FoSER Michael W. Whalen, Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser
2010	—	`ch.`	Model Checking Information Flow. Design and Verification of Microprocessor Systems for High-Assurance Applications Michael W. Whalen, David A. Greve, Lucas G. Wagner
2010	J	`jnl`	Software model checking takes off. Commun. ACM Steven P. Miller, Michael W. Whalen, Darren D. Cofer
2009	C	`conf`	Development of Security Software: A High Assurance Methodology. ICFEM David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen
2008	J	`jnl`	Model-Checking of Safety-Critical Software for Avionics. ERCIM News Darren D. Cofer, Michael W. Whalen, Steven P. Miller
2008	C	`conf`	Requirements Coverage as an Adequacy Measure for Conformance Testing. ICFEM Ajitha Rajan, Michael W. Whalen, Matt Staats, Mats Per Erik Heimdahl
2008	A*	`conf`	The effect of program and model structure on mc/dc test adequacy coverage. ICSE Ajitha Rajan, Michael W. Whalen, Mats Per Erik Heimdahl
2007	C	`conf`	Integration of Formal Analysis into a Model-Based Software Development Process. FMICS Michael W. Whalen, Darren D. Cofer, Steven P. Miller, Bruce H. Krogh, Walter Storm
2007	—	`conf`	Model Validation using Automatically Generated Requirements-Based Tests. HASE Ajitha Rajan, Michael W. Whalen, Mats Per Erik Heimdahl
2006	A	`conf`	Coverage metrics for requirements-based testing. ISSTA Michael W. Whalen, Ajitha Rajan, Mats Per Erik Heimdahl, Steven P. Miller
2006	J	`jnl`	Proving the shalls. Int. J. Softw. Tools Technol. Transf. Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl
2005	J	`jnl`	Deviation Analysis: A New Use of Model Checking. Autom. Softw. Eng. Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen
2003	—	`conf`	Certification Support for Automatically Generated Programs. HICSS Johann Schumann, Bernd Fischer, Michael W. Whalen, Jon Whittle
2003	A	`conf`	NIMBUS: A Tool for Specification Centered Development. RE Mats Per Erik Heimdahl, Michael W. Whalen, Jeffrey M. Thompson
2002	A	`conf`	AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. CADE Michael W. Whalen, Johann Schumann, Bernd Fischer
2002	A*	`conf`	Deviation Analysis Through Model Checking. ASE Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen
2002	—	`conf`	Synthesizing Certified Code. FME Michael W. Whalen, Johann Schumann, Bernd Fischer
2000	A*	`conf`	High-integrity code generation for state-based formalisms. ICSE Michael W. Whalen
2000	J	`jnl`	Requirements Capture and Evaluation in Nimbus: The Light-Control Case Study. J. Univers. Comput. Sci. Jeffrey M. Thompson, Michael W. Whalen, Mats Per Erik Heimdahl
1999	A*	`conf`	An Approach to Automatic Code Generation for Safety-Critical Systems. ASE Michael W. Whalen, Mats Per Erik Heimdahl
1999	—	`conf`	On the Requirements of High-Integrity Code Generation. HASE Michael W. Whalen, Mats Per Erik Heimdahl
1998	—	`conf`	On the Effectiveness of Slicing Hierarchical State Machines: A Case Study. EUROMICRO Mats Per Erik Heimdahl, Jeffrey M. Thompson, Michael W. Whalen
1997	—	`conf`	Reduction and Slicing of Hierarchical State Machines. ESEC / SIGSOFT FSE Mats Per Erik Heimdahl, Michael W. Whalen
1995	J	`jnl`	Handprinted word recognition on a NIST data set. Mach. Vis. Appl. Paul D. Gader, Michael W. Whalen, Margaret Ganzberger, Daniel J. Hepp
1991	J	`jnl`	Recognition of handwritten digits using template and model matching. Pattern Recognit. Paul D. Gader, Brian Forester, Margaret Ganzberger, Andrew M. Gillies, Brian T. Mitchell, Michael W. Whalen, Todd Yocum