John Hatcliff

Publication Activity (10 Years)

Years Active: 1992-2024
Publications (10 Years): 24

Top Venues

SAFECOMP Workshops

ISoLA (1)

FMICS

ISoLA

Publications

Robby, John Hatcliff, Jason Belt
Logika: The Sireum Verification Framework. FMICS (2024)
John Hatcliff, Jason Belt, Robby, David S. Hardin
Integrated Contract-Based Unit and System Testing for Component-Based Systems. NFM (2024)
John Hatcliff, Jason Belt, Robby, Jacob Legg, Danielle Stewart, Todd Carpenter
Automated Property-Based Testing from AADL Component Contracts. FMICS (2023)
Erika Ábrahám, Stefan Hallerstede, John Hatcliff, Danielle Stewart, Noah Abou El Wafa
Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041). Dagstuhl Reports 13 (1) (2023)
Stefan Hallerstede, John Hatcliff
A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime. FACS (2023)
Jason Belt, John Hatcliff, Robby, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren D. Cofer, David S. Hardin, Karl Hoech, Konrad Slind, Ihor Kuz, Kent McLeod
Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. 134 (2023)
Jérôme Hugues, Lutz Wrage, John Hatcliff, Danielle Stewart
Mechanization of a Large DSML: An Experiment with AADL and Coq. MEMOCODE (2022)
Darren D. Cofer, Isaac Amundson, Junaid Babar, David S. Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer, John Shackleton
Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 20 (3) (2022)
John Hatcliff, Jérôme Hugues, Danielle Stewart, Lutz Wrage
Formalization of the AADL Run-Time Services. ISoLA (2) (2022)
Hariharan Thiagarajan, John Hatcliff, Robby
Awas: AADL information flow and error propagation analysis framework. Innov. Syst. Softw. Eng. 18 (4) (2022)
Mahsa Zarneshan, Fatemeh Ghassemi, Ehsan Khamespanah, Marjan Sirjani, John Hatcliff
Specification and Verification of Timing Properties in Interoperable Medical Systems. Log. Methods Comput. Sci. 18 (2) (2022)
John Hatcliff, Jason Belt, Robby, Todd Carpenter
HAMR: An AADL Multi-platform Code Generation Toolset. ISoLA (2021)
Robby, John Hatcliff
Slang: The Sireum Programming Language. ISoLA (2021)
Hariharan Thiagarajan, Brian R. Larson, John Hatcliff, Yi Zhang
Model-Based Risk Analysis for an Open-Source PCA Pump Using AADL Error Modeling. IMBSA (2020)
Mahsa Zarneshan, Fatemeh Ghassemi, Ehsan Khamespanah, Marjan Sirjani, John Hatcliff
Specification and Verification of Timing Properties in Interoperable Medical Systems. CoRR (2020)
Hariharan Thiagarajan, John Hatcliff, Robby
Awas: AADL Information Flow and Error Propagation Analysis Framework. ECSA Companion (2020)
John Hatcliff, Brian R. Larson, Todd Carpenter, Paul L. Jones, Yi Zhang, Joseph Jorgens
The open PCA pump project: an exemplar open source medical device as a community resource. SIGBED Rev. 16 (2) (2019)
John Hatcliff, Brian R. Larson, Jason Belt, Robby, Yi Zhang
A Unified Approach for Modeling, Developing, and Assuring Critical Systems. ISoLA (1) (2018)
Robby, John Hatcliff, Jason Belt
Model-Based Development for High-Assurance Embedded Systems. ISoLA (1) (2018)
Yi Zhang, Brian R. Larson, John Hatcliff
Assurance Case Considerations for Interoperable Medical Systems. SAFECOMP Workshops (2018)
Todd Carpenter, John Hatcliff, Eugene Y. Vasserman
A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices. SafeThings@SenSys (2017)
Sam Procter, Eugene Y. Vasserman, John Hatcliff
SAFE and Secure: Deeply Integrating Security in a New Hazard Analysis. ARES (2017)
Xiaolong Wang, Richard Habeeb, Xinming Ou, Siddharth Amaravadi, John Hatcliff, Masaaki Mizuno, Mitchell L. Neilsen, S. Raj Rajagopalan, Srivatsan Varadarajan
Enhanced Security of Building Automation Systems Through Microkernel-Based Controller Platforms. ICDCS Workshops (2017)
Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu
Focused Certification of an Industrial Compilation and Static Verification Toolchain. SEFM (2017)
Sam Procter, John Hatcliff, Sandy Weininger, Anura Fernando
Error Type Refinement for Assurance of Families of Platform-Based Systems. SAFECOMP Workshops (2015)
Venkatesh-Prasad Ranganath, Yu Jin Kim, John Hatcliff, Robby
Communication patterns for interconnecting and composing medical systems. EMBC (2015)
Andrew L. King, Lu Feng, Sam Procter, Sanjian Chen, Oleg Sokolsky, John Hatcliff, Insup Lee
Towards Assurance for Plug & Play Medical Systems. SAFECOMP (2015)
Brian R. Larson, Yi Zhang, Stephen C. Barrett, John Hatcliff, Paul L. Jones
Enabling Safe Interoperation by Medical Device Virtual Integration. IEEE Des. Test 32 (5) (2015)
Yu Jin Kim, Sam Procter, John Hatcliff, Venkatesh-Prasad Ranganath, Robby
Ecosphere Principles for Medical Application Platforms. ICHI (2015)
Sam Procter, John Hatcliff
An architecturally-integrated, systems-based hazard analysis for medical applications. MEMOCODE (2014)
Sam Procter, John Hatcliff, Robby
Towards an AADL-Based Definition of App Architecture for Medical Application Platforms. FHIES/SEHC (2014)
John Hatcliff, Alan Wassyng, Tim Kelly, Cyrille Comar, Paul L. Jones
Certifiably safe software-dependent systems: challenges and directions. FOSE (2014)
Pierre Courtieu, Maria-Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings
Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. HILT (2013)
Darren D. Cofer, John Hatcliff, Michaela Huhn, Mark Lawford
Software Certification: Methods and Tools (Dagstuhl Seminar 13051). Dagstuhl Reports 3 (1) (2013)
Eugene Y. Vasserman, John Hatcliff
Foundational Security Principles for Medical Application Platforms - (Extended Abstract). WISA (2013)
Brian R. Larson, Patrice Chalin, John Hatcliff
BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. NASA Formal Methods (2013)
John Hatcliff, Robby, Patrice Chalin, Jason Belt
Explicating symbolic execution (xSymExe): an evidence-based verification framework. ICSE (2013)
Brian R. Larson, John Hatcliff, Patrice Chalin
Open source patient-controlled analgesic pump requirements documentation. SEHC@ICSE (2013)
Brian R. Larson, John Hatcliff, Kim R. Fowler, Julien Delange
Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device. HILT (2013)
Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, BaekGyu Kim, Andrew L. King, Margaret Mullen-Fortino, Soojin Park, Alex Roederer, Krishna K. Venkatasubramanian
Challenges and Research Directions in Medical Cyber-Physical Systems. Proc. IEEE 100 (1) (2012)
John Hatcliff, Andrew L. King, Insup Lee, Alasdair Macdonald, Anura Fernando, Michael Robkin, Eugene Y. Vasserman, Sandy Weininger, Julian M. Goldman
Rationale and Architecture Principles for Medical Application Platforms. ICCPS (2012)
Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. POST (2012)
Kejia Li, Steve Warren, John Hatcliff
Component-based app design for platform-oriented devices in a medical device coordination framework. IHI (2012)
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
Behavioral interface specification languages. ACM Comput. Surv. 44 (3) (2012)
Hariharan Thiagarajan, John Hatcliff, Jason Belt, Robby
Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. SCAM (2012)
Jason Belt, Patrice Chalin, John Hatcliff, Robby
Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. HILT (2012)
Jason Belt, Robby, Patrice Chalin, John Hatcliff, Xianghua Deng
Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. NASA Formal Methods (2012)
Brian R. Larson, John Hatcliff, Sam Procter, Patrice Chalin
Requirements specification for apps in medical application platforms. SEHC@ICSE (2012)
Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. NASA Formal Methods (2011)
Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
Enhancing spark's contract checking facilities using symbolic execution. SIGAda (2011)
Georg Jung, John Hatcliff
A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. Sci. Comput. Program. 75 (7) (2010)
Torben Amtoft, John Hatcliff, Edwin Rodríguez
Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. ESOP (2010)
Alan Wassyng, Mark Lawford, T. S. E. Maibaum, Jens H. Weber, John Hatcliff
Software certification consortium: certification methods for safety-critical software. CASCON (2010)
Andrew L. King, David Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, Sam Procter
Prototyping closed loop physiologic control with the medical device coordination framework. SEHC@ICSE (2010)
Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
A publish-subscribe architecture and component-based programming model for medical device interoperability. SIGBED Rev. 6 (2) (2009)
Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
An open test bed for medical device integration and coordination. ICSE Companion (2009)
Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
Demonstration of a medical device integration and coordination framework. ICSE Companion (2009)
John Hatcliff, Mats Per Erik Heimdahl, Mark Lawford, T. S. E. Maibaum, Alan Wassyng, Fred L. Wurden
A Software Certification Consortium and its Top 9 Hurdles. Electron. Notes Theor. Comput. Sci. 238 (4) (2009)
Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve
Specification and Checking of Software Contracts for Conditional Information Flow. FM (2008)
John Hatcliff
Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. ICFEM (2008)
Georg Jung, John Hatcliff
A correlation framework for the CORBA component model. Int. J. Softw. Tools Technol. Transf. 9 (5-6) (2007)
Georg Jung, John Hatcliff
A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. GPCE (2007)
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, John Hatcliff, Matthew B. Dwyer
A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29 (5) (2007)
Venkatesh Prasad Ranganath, John Hatcliff
Slicing concurrent Java programs using Indus and Kaveri. Int. J. Softw. Tools Technol. Transf. 9 (5-6) (2007)
Xianghua Deng, Robby, John Hatcliff
Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. SEFM (2007)
Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser
Formal Software Analysis Emerging Trends in Software Model Checking. FOSE (2007)
Hubert Garavel, John Hatcliff
Why you should definitely read this special section. Int. J. Softw. Tools Technol. Transf. 8 (1) (2006)
Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
Checking JML specifications using an extensible software model checking framework. Int. J. Softw. Tools Technol. Transf. 8 (3) (2006)
Xianghua Deng, Robby, John Hatcliff
Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. ISoLA (2006)
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. TACAS (2006)
Arvind S. Krishna, Aniruddha S. Gokhale, Douglas C. Schmidt, Venkatesh Prasad Ranganath, John Hatcliff
Towards highly optimized real-time middleware for software product-line architectures. SIGBED Rev. 3 (1) (2006)
Mark W. Bailey, John Hatcliff, Frank Tip
PEPM 2006 paper abstracts. ACM SIGPLAN Notices 41 (3) (2006)
Robby, Matthew B. Dwyer, John Hatcliff
Domain-specific Model Checking Using The Bogor Framework. ASE (2006)
Robby, Matthew B. Dwyer, John Hatcliff
Bogor: A Flexible Framework for Creating Software Model Checkers. TAIC PART (2006)
Adam Childs, Jesse Greenwald, Georg Jung, Matthew Hoosier, John Hatcliff
CALM and Cadena: Metamodeling for Component-Based Product-Line Development. Computer 39 (2) (2006)
John Hatcliff, Insup Lee, Oleg Sokolsky
Introduction to special issue. SIGBED Rev. 3 (4) (2006)
Hubert Garavel, John Hatcliff
TACAS 2003 Special Issue - Preface. Theor. Comput. Sci. 354 (2) (2006)
Insup Lee, George J. Pappas, Rance Cleaveland, John Hatcliff, Bruce H. Krogh, Peter Lee, Harvey Rubin, Lui Sha
High-Confidence Medical Device Software and Systems. Computer 39 (4) (2006)
Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby
Extending JML for Modular Specification and Verification of Multi-threaded Programs. ECOOP (2005)
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff
A New Foundation for Control-Dependence and Slicing for Modern Program Structures. ESOP (2005)
Ganeshan Jayaraman, Venkatesh Prasad Ranganath, John Hatcliff
Kaveri: Delivering the Indus Java Program Slicer to Eclipse. FASE (2005)
Radu Iosif, Matthew B. Dwyer, John Hatcliff
Translating Java for Multiple Model Checkers: The Bandera Back-End. Formal Methods Syst. Des. 26 (2) (2005)
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. CAV (2005)
Matthew Hoosier, Matthew B. Dwyer, Robby, John Hatcliff
A Case Study in Domain-Customized Model Checking for Real-Time Component Software. ISoLA (2004)
Venkatesh Prasad Ranganath, John Hatcliff
Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. CC (2004)
Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff, Robby
A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. CASSIS (2004)
Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno
SyncGen: An Aspect-Oriented Framework for Synchronization. TACAS (2004)
John Hatcliff, Robby, Matthew B. Dwyer
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. VMCAI (2004)
Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath
A Correlation Framework for the CORBA Component Model. FASE (2004)
Adam Childs, Jesse Greenwald, Venkatesh Prasad Ranganath, Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Prashant Shanti, Gurdip Singh
Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems. FASE (2004)
Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
Checking Strong Specifications Using an Extensible Software Model Checking Framework. TACAS (2004)
Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer
A Case Study in Domain-customized Model Checking for Real-time Component Software. ISoLA (Preliminary proceedings) (2004)
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier
Supporting model checking education using BOGOR/Eclipse. eTX (2004)
Matthew B. Dwyer, John Hatcliff, Robby, Venkatesh Prasad Ranganath
Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs. Formal Methods Syst. Des. 25 (2-3) (2004)
Matthew B. Dwyer, Robby, Xianghua Deng, John Hatcliff
Space Reductions for Model Checking Quasi-Cyclic Systems. EMSOFT (2003)
John Hatcliff, Xianghua Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath
Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. ICSE (2003)
John Hatcliff, William Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath, Robby
Slicing and partial evaluation of CORBA component model designs for avionics system. PEPM (2003)
Robby, Matthew B. Dwyer, John Hatcliff
Bogor: an extensible and highly-modular software model checking framework. ESEC / SIGSOFT FSE (2003)
Venkatesh Prasad Ranganath, Adam Childs, Jesse Greenwald, Matthew B. Dwyer, John Hatcliff, Gurdip Singh
Cadena: enabling CCM-based application development in Eclipse. eTX (2003)
Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif
Space-Reduction Strategies for Model Checking Dynamic Software. Electron. Notes Theor. Comput. Sci. 89 (3) (2003)

John Hatcliff.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

John Hatcliff