John Hatcliff

Orcid: 0009-0001-3782-7082

Affiliations:
  • Kansas State Uniersity, Manhattan, KS, USA


According to our database1, John Hatcliff authored at least 130 papers between 1992 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Teaching with Logika: Conceiving and Constructing Correct Software.
Proceedings of the Formal Methods Teaching - 6th Formal Methods Teaching Workshop, 2024

Integrated Contract-Based Unit and System Testing for Component-Based Systems.
Proceedings of the NASA Formal Methods - 16th International Symposium, 2024

Logika: The Sireum Verification Framework.
Proceedings of the Formal Methods for Industrial Critical Systems, 2024

2023
Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041).
Dagstuhl Reports, January, 2023

Model-driven development for the seL4 microkernel using the HAMR framework.
J. Syst. Archit., 2023

Automated Property-Based Testing from AADL Component Contracts.
Proceedings of the Formal Methods for Industrial Critical Systems, 2023

A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime.
Proceedings of the Formal Aspects of Component Software - 19th International Conference, 2023

2022
Specification and Verification of Timing Properties in Interoperable Medical Systems.
Log. Methods Comput. Sci., 2022

Awas: AADL information flow and error propagation analysis framework.
Innov. Syst. Softw. Eng., 2022

Cyberassured Systems Engineering at Scale.
IEEE Secur. Priv., 2022

Mechanization of a Large DSML: An Experiment with AADL and Coq.
Proceedings of the 20th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2022

Formalization of the AADL Run-Time Services.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

2021
Slang: The Sireum Programming Language.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 2021

HAMR: An AADL Multi-platform Code Generation Toolset.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 2021

2020
Model-Based Risk Analysis for an Open-Source PCA Pump Using AADL Error Modeling.
Proceedings of the Model-Based Safety and Assessment - 7th International Symposium, 2020

2019
The open PCA pump project: an exemplar open source medical device as a community resource.
SIGBED Rev., 2019

2018
Assurance Case Considerations for Interoperable Medical Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2018

Model-Based Development for High-Assurance Embedded Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

A Unified Approach for Modeling, Developing, and Assuring Critical Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

2017
A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices.
Proceedings of the 1st ACM Workshop on the Internet of Safe Things, 2017

Focused Certification of an Industrial Compilation and Static Verification Toolchain.
Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

Enhanced Security of Building Automation Systems Through Microkernel-Based Controller Platforms.
Proceedings of the 37th IEEE International Conference on Distributed Computing Systems Workshops, 2017

SAFE and Secure: Deeply Integrating Security in a New Hazard Analysis.
Proceedings of the 12th International Conference on Availability, Reliability and Security, Reggio Calabria, Italy, August 29, 2017

2015
Enabling Safe Interoperation by Medical Device Virtual Integration.
IEEE Des. Test, 2015

Error Type Refinement for Assurance of Families of Platform-Based Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2015

Towards Assurance for Plug & Play Medical Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2015

Ecosphere Principles for Medical Application Platforms.
Proceedings of the 2015 International Conference on Healthcare Informatics, 2015

Communication patterns for interconnecting and composing medical systems.
Proceedings of the 37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society, 2015

2014
An architecturally-integrated, systems-based hazard analysis for medical applications.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Certifiably safe software-dependent systems: challenges and directions.
Proceedings of the on Future of Software Engineering, 2014

Towards an AADL-Based Definition of App Architecture for Medical Application Platforms.
Proceedings of the Software Engineering in Health Care - 4th International Symposium, 2014

2013
Software Certification: Methods and Tools (Dagstuhl Seminar 13051).
Dagstuhl Reports, 2013

Foundational Security Principles for Medical Application Platforms - (Extended Abstract).
Proceedings of the Information Security Applications - 14th International Workshop, 2013

Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device.
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq.
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software.
Proceedings of the NASA Formal Methods, 2013

Open source patient-controlled analgesic pump requirements documentation.
Proceedings of the 5th International Workshop on Software Engineering in Health Care, 2013

Explicating symbolic execution (xSymExe): an evidence-based verification framework.
Proceedings of the 35th International Conference on Software Engineering, 2013

2012
Challenges and Research Directions in Medical Cyber-Physical Systems.
Proc. IEEE, 2012

Behavioral interface specification languages.
ACM Comput. Surv., 2012

Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan.
Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK.
Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation, 2012

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow.
Proceedings of the Principles of Security and Trust - First International Conference, 2012

Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems.
Proceedings of the NASA Formal Methods, 2012

Component-based app design for platform-oriented devices in a medical device coordination framework.
Proceedings of the ACM International Health Informatics Symposium, 2012

Requirements specification for apps in medical application platforms.
Proceedings of the 4th International Workshop on Software Engineering in Health Care, 2012

Rationale and Architecture Principles for Medical Application Platforms.
Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, 2012

2011
Enhancing spark's contract checking facilities using symbolic execution.
Proceedings of the 2011 Annual ACM SIGAda International Conference on Ada, 2011

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution.
Proceedings of the NASA Formal Methods, 2011

2010
A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures.
Sci. Comput. Program., 2010

Prototyping closed loop physiologic control with the medical device coordination framework.
Proceedings of the 2010 ICSE Workshop on Software Engineering in Health Care, 2010

Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays.
Proceedings of the Programming Languages and Systems, 2010

Software certification consortium: certification methods for safety-critical software.
Proceedings of the 2010 conference of the Centre for Advanced Studies on Collaborative Research, 2010

Specification and Checking of Software Contracts for Conditional Information Flow.
Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009
A publish-subscribe architecture and component-based programming model for medical device interoperability.
SIGBED Rev., 2009

Demonstration of a medical device integration and coordination framework.
Proceedings of the 31st International Conference on Software Engineering, 2009

An open test bed for medical device integration and coordination.
Proceedings of the 31st International Conference on Software Engineering, 2009

2008
A Software Certification Consortium and its Top 9 Hurdles.
Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems, 2008

Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows.
Proceedings of the Formal Methods and Software Engineering, 2008

Specification and Checking of Software Contracts for Conditional Information Flow.
Proceedings of the FM 2008: Formal Methods, 2008

2007
A new foundation for control dependence and slicing for modern program structures.
ACM Trans. Program. Lang. Syst., 2007

Slicing concurrent Java programs using Indus and Kaveri.
Int. J. Softw. Tools Technol. Transf., 2007

A correlation framework for the CORBA component model.
Int. J. Softw. Tools Technol. Transf., 2007

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs.
Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Formal Software Analysis Emerging Trends in Software Model Checking.
Proceedings of the International Conference on Software Engineering, 2007

2006
TACAS 2003 Special Issue - Preface.
Theor. Comput. Sci., 2006

Checking JML specifications using an extensible software model checking framework.
Int. J. Softw. Tools Technol. Transf., 2006

Why you should definitely read this special section.
Int. J. Softw. Tools Technol. Transf., 2006

PEPM 2006 paper abstracts.
ACM SIGPLAN Notices, 2006

Towards highly optimized real-time middleware for software product-line architectures.
SIGBED Rev., 2006

Introduction to special issue.
SIGBED Rev., 2006

High-Confidence Medical Device Software and Systems.
Computer, 2006

CALM and Cadena: Metamodeling for Component-Based Product-Line Development.
Computer, 2006

Bogor: A Flexible Framework for Creating Software Model Checkers.
Proceedings of the Testing: Academia and Industry Conference, 2006

Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Domain-specific Model Checking Using The Bogor Framework.
Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 2006

Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution.
Proceedings of the Leveraging Applications of Formal Methods, 2006

2005
Translating Java for Multiple Model Checkers: The Bandera Back-End.
Formal Methods Syst. Des., 2005

Kaveri: Delivering the Indus Java Program Slicer to Eclipse.
Proceedings of the Fundamental Approaches to Software Engineering, 2005

Extending JML for Modular Specification and Verification of Multi-threaded Programs.
Proceedings of the ECOOP 2005, 2005

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

An Integrated Model-Driven Development Environment for Composing and Validating Distributed Real-Time and Embedded Systems.
Proceedings of the Model-Driven Software Development, 2005

2004
Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs.
Formal Methods Syst. Des., 2004

Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking.
Proceedings of the Verification, 2004

Checking Strong Specifications Using an Extensible Software Model Checking Framework.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

SyncGen: An Aspect-Oriented Framework for Synchronization.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

A Case Study in Domain-customized Model Checking for Real-time Component Software.
Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

A Correlation Framework for the CORBA Component Model.
Proceedings of the Fundamental Approaches to Software Engineering, 2004

Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2004

Supporting model checking education using BOGOR/Eclipse.
Proceedings of the 2004 OOPSLA workshop on Eclipse Technology eXchange, 2004

Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs.
Proceedings of the Compiler Construction, 13th International Conference, 2004

A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking.
Proceedings of the Construction and Analysis of Safe, 2004

2003
Space-Reduction Strategies for Model Checking Dynamic Software.
Proceedings of the 2003 Workshop on Software Model Checking, 2003

Bogor: an extensible and highly-modular software model checking framework.
Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, 2003

Slicing and partial evaluation of CORBA component model designs for avionics system.
Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003

Cadena: enabling CCM-based application development in Eclipse.
Proceedings of the 2003 OOPSLA Workshop on Eclipse Technology eXchange, 2003

Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems.
Proceedings of the 25th International Conference on Software Engineering, 2003

Space Reductions for Model Checking Quasi-Cyclic Systems.
Proceedings of the Embedded Software, Third International Conference, 2003

2002
Expressing checkable properties of dynamic systems: the Bandera Specification Language.
Int. J. Softw. Tools Technol. Transf., 2002

Invariant-based specification, synthesis, and verification of synchronization in concurrent programs.
Proceedings of the 24th International Conference on Software Engineering, 2002

Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software.
Proceedings of the Formal Methods for Components and Objects, 2002

Foundations of the Bandera Abstraction Tools.
Proceedings of the Essence of Computation, Complexity, Analysis, 2002

2001
Weak normalization implies strong normalization in a class of non-dependent pure type systems.
Theor. Comput. Sci., 2001

An induction principle for pure type systems.
Theor. Comput. Sci., 2001

Tool-Supported Program Abstraction for Finite-State Verification.
Proceedings of the 23rd International Conference on Software Engineering, 2001

Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software.
Proceedings of the CONCUR 2001, 2001

2000
Adapting programming languages technologies for finite-state verification.
ACM SIGSOFT Softw. Eng. Notes, 2000

Slicing Software for Model Construction.
High. Order Symb. Comput., 2000

A Language Framework for Expressing Checkable Properties of Dynamic Software.
Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

Bandera: a source-level interface for model checking Java programs.
Proceedings of the 22nd International Conference on on Software Engineering, 2000

Bandera: extracting finite-state models from Java source code.
Proceedings of the 22nd International Conference on on Software Engineering, 2000

1999
CPS Translations and Applications: The Cube and Beyond.
High. Order Symb. Comput., 1999

A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives.
Proceedings of the Static Analysis, 6th International Symposium, 1999

Slicing Software for Model Construction.
Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 1999

1998
Foundations for Partial Evaluation of Functional Programs with Computational Effects.
ACM Comput. Surv., 1998

Using Partial Evaluation to Enable Verification of Concurrent Software.
ACM Comput. Surv., 1998

Staging Static Analyses Using Abstraction-Based Program Specialization.
Proceedings of the Principles of Declarative Programming, 10th International Symposium, 1998

An Introduction to Online and Offline Partial Evaluation using a Simple Flowchart Language.
Proceedings of the Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29, 1998

Generalization in Hierarchies of Online Program Specialization Systems.
Proceedings of the Logic Programming Synthesis and Transformation, 1998

1997
A Computational Formalization for Partial Evaluation.
Math. Struct. Comput. Sci., 1997

Thunks and the lambda-Calculus.
J. Funct. Program., 1997

Monadic Type Systems: Pure Type Systems for Impure Settings.
Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

A notion of classical pure type system.
Proceedings of the Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, 1997

Reflections on Reflections.
Proceedings of the Programming Languages: Implementations, 1997

1996
Reasoning about Hierarchies of Online Program Specialization Systems.
Proceedings of the Partial Evaluation, International Seminar, 1996

1995
Mechanically Verifying the Correctness of an Offline Partial Evaluator
Proceedings of the Programming Languages: Implementations, 1995

1994
A Generic Account of Continuation-Passing Styles.
Proceedings of the Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994

1993
On the Transformation between Direct and Continuation Semantics.
Proceedings of the Mathematical Foundations of Programming Semantics, 1993

1992
CPS-Transformation After Strictness Analysis.
LOPLAS, 1992

Thunks (Continued).
Proceedings of the Actes WSA'92 Workshop on Static Analysis (Bordeaux, 1992


  Loading...