| 2025 | FMICS | Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. | Stefan Hallerstede, Robby, John Hatcliff, Jason Belt, David S. Hardin |
| 2025 | FMICS | End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR. | John Hatcliff, Jason Belt, Robby, Clint McKenzie, Catalina Liang |
| 2024 | FMICS | Logika: The Sireum Verification Framework. | Robby, John Hatcliff, Jason Belt |
| 2023 | FMICS | Automated Property-Based Testing from AADL Component Contracts. | John Hatcliff, Jason Belt, Robby, Jacob Legg, Danielle Stewart, Todd Carpenter |
| 2022 | ISoLA | Formalization of the AADL Run-Time Services. | John Hatcliff, Jrme Hugues, Danielle Stewart, Lutz Wrage |
| 2022 | MEMOCODE | Mechanization of a Large DSML: An Experiment with AADL and Coq. | Jrme Hugues, Lutz Wrage, John Hatcliff, Danielle Stewart |
| 2021 | ISoLA | HAMR: An AADL Multi-platform Code Generation Toolset. | John Hatcliff, Jason Belt, Robby, Todd Carpenter |
| 2021 | ISoLA | Slang: The Sireum Programming Language. | Robby, John Hatcliff |
| 2020 | ECSA | Awas: AADL Information Flow and Error Propagation Analysis Framework. | Hariharan Thiagarajan, John Hatcliff, Robby |
| 2018 | ISoLA | A Unified Approach for Modeling, Developing, and Assuring Critical Systems. | John Hatcliff, Brian R. Larson, Jason Belt, Robby, Yi Zhang |
| 2018 | ISoLA | Model-Based Development for High-Assurance Embedded Systems. | Robby, John Hatcliff, Jason Belt |
| 2018 | SAFECOMP | Assurance Case Considerations for Interoperable Medical Systems. | Yi Zhang, Brian R. Larson, John Hatcliff |
| 2017 | SENSYS | A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices. | Todd Carpenter, John Hatcliff, Eugene Y. Vasserman |
| 2017 | SEFM | Focused Certification of an Industrial Compilation and Static Verification Toolchain. | Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu |
| 2015 | SAFECOMP | Towards Assurance for Plug & Play Medical Systems. | Andrew L. King, Lu Feng, Sam Procter, Sanjian Chen, Oleg Sokolsky, John Hatcliff, Insup Lee |
| 2015 | SAFECOMP | Error Type Refinement for Assurance of Families of Platform-Based Systems. | Sam Procter, John Hatcliff, Sandy Weininger, Anura Fernando |
| 2014 | ICSE | Certifiably safe software-dependent systems: challenges and directions. | John Hatcliff, Alan Wassyng, Tim Kelly, Cyrille Comar, Paul L. Jones |
| 2014 | MEMOCODE | An architecturally-integrated, systems-based hazard analysis for medical applications. | Sam Procter, John Hatcliff |
| 2013 | ICSE | Explicating symbolic execution (xSymExe): an evidence-based verification framework. | John Hatcliff, Robby, Patrice Chalin, Jason Belt |
| 2013 | ICSE | Open source patient-controlled analgesic pump requirements documentation. | Brian R. Larson, John Hatcliff, Patrice Chalin |
| 2013 | WISA | Foundational Security Principles for Medical Application Platforms - (Extended Abstract). | Eugene Y. Vasserman, John Hatcliff |
| 2012 | ICSE | Requirements specification for apps in medical application platforms. | Brian R. Larson, John Hatcliff, Sam Procter, Patrice Chalin |
| 2012 | SCAM | Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. | Hariharan Thiagarajan, John Hatcliff, Jason Belt, Robby |
| 2010 | ESOP | Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. | Torben Amtoft, John Hatcliff, Edwin Rodrguez |
| 2010 | ICSE | Prototyping closed loop physiologic control with the medical device coordination framework. | Andrew L. King, David Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, Sam Procter |
| 2009 | ICSE | An open test bed for medical device integration and coordination. | Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger |
| 2009 | ICSE | Demonstration of a medical device integration and coordination framework. | Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger |
| 2008 | FM | Specification and Checking of Software Contracts for Conditional Information Flow. | Torben Amtoft, John Hatcliff, Edwin Rodrguez, Robby, Jonathan Hoag, David A. Greve |
| 2008 | ICFEM | Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. | John Hatcliff |
| 2007 | GPCE | A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. | Georg Jung, John Hatcliff |
| 2007 | ICSE | Formal Software Analysis Emerging Trends in Software Model Checking. | Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser |
| 2007 | SEFM | Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. | Xianghua Deng, Robby, John Hatcliff |
| 2006 | ISoLA | Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. | Xianghua Deng, Robby, John Hatcliff |
| 2006 | TACAS | Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. | Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine |
| 2005 | CAV | Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. | Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby |
| 2005 | ECOOP | Extending JML for Modular Specification and Verification of Multi-threaded Programs. | Edwin Rodrguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby |
| 2005 | ESOP | A New Foundation for Control-Dependence and Slicing for Modern Program Structures. | Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff |
| 2005 | FASE | Kaveri: Delivering the Indus Java Program Slicer to Eclipse. | Ganeshan Jayaraman, Venkatesh Prasad Ranganath, John Hatcliff |
| 2004 | CC | Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. | Venkatesh Prasad Ranganath, John Hatcliff |
| 2004 | FASE | Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems. | Adam Childs, Jesse Greenwald, Venkatesh Prasad Ranganath, Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Prashant Shanti, Gurdip Singh |
| 2004 | FASE | A Correlation Framework for the CORBA Component Model. | Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath |
| 2004 | ISoLA | A Case Study in Domain-Customized Model Checking for Real-Time Component Software. | Matthew Hoosier, Matthew B. Dwyer, Robby, John Hatcliff |
| 2004 | ISoLA | A Case Study in Domain-customized Model Checking for Real-time Component Software. | Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer |
| 2004 | TACAS | SyncGen: An Aspect-Oriented Framework for Synchronization. | Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno |
| 2004 | TACAS | Checking Strong Specifications Using an Extensible Software Model Checking Framework. | Robby, Edwin Rodrguez, Matthew B. Dwyer, John Hatcliff |
| 2004 | VMCAI | Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. | John Hatcliff, Robby, Matthew B. Dwyer |
| 2003 | EMSOFT | Space Reductions for Model Checking Quasi-Cyclic Systems. | Matthew B. Dwyer, Robby, Xianghua Deng, John Hatcliff |
| 2003 | ICSE | Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. | John Hatcliff, Xianghua Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath |
| 2003 | OOPSLA | Cadena: enabling CCM-based application development in Eclipse. | Venkatesh Prasad Ranganath, Adam Childs, Jesse Greenwald, Matthew B. Dwyer, John Hatcliff, Gurdip Singh |
| 2003 | PEPM | Slicing and partial evaluation of CORBA component model designs for avionics system. | John Hatcliff, William Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath, Robby |
| 2002 | ICSE | Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. | Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno |
| 2001 | CONCUR | Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. | John Hatcliff, Matthew B. Dwyer |
| 2001 | ICSE | Tool-Supported Program Abstraction for Finite-State Verification. | Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng, Willem Visser |
| 2000 | ICSE | Bandera: extracting finite-state models from Java source code. | James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng |
| 2000 | ICSE | Bandera: a source-level interface for model checking Java programs. | James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby |
| 1999 | PEPM | Slicing Software for Model Construction. | Matthew B. Dwyer, John Hatcliff |
| 1999 | SAS | A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives. | John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, Hongjun Zheng |
| 1998 | LOPSTR | Generalization in Hierarchies of Online Program Specialization Systems. | Robert Glck, John Hatcliff, Jesper Jrgensen |
| 1998 | PEPM | An Introduction to Online and Offline Partial Evaluation using a Simple Flowchart Language. | John Hatcliff |
| 1994 | POPL | A Generic Account of Continuation-Passing Styles. | John Hatcliff, Olivier Danvy |
| 1993 | MFPS | On the Transformation between Direct and Continuation Semantics. | Olivier Danvy, John Hatcliff |
| 1992 | SAS | Thunks (Continued). | Olivier Danvy, John Hatcliff |