Thunks (Continued). - Olivier Danvy; John Hatcliff (WSA, 1992)

CPS-Transformation After Strictness Analysis. - Olivier Danvy; John Hatcliff (LOPLAS, 1992)

On the Transformation between Direct and Continuation Semantics. - Olivier Danvy; John Hatcliff (MFPS, 1993)

A Generic Account of Continuation-Passing Styles. - John Hatcliff; Olivier Danvy (POPL, 1994)

Mechanically Verifying the Correctness of an Offline Partial Evaluator - John Hatcliff (PLILP, 1995)

Reasoning about Hierarchies of Online Program Specialization Systems. - John Hatcliff; Robert Glück (Dagstuhl Seminar on Partial Evaluation, 1996)

Reflections on Reflections. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (PLILP, 1997)

A notion of classical pure type system. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (MFPS, 1997)

Monadic Type Systems: Pure Type Systems for Impure Settings. - Gilles Barthe; John Hatcliff; Peter Thiemann 001 (HOOTS, 1997)

Thunks and the lambda-Calculus. - John Hatcliff; Olivier Danvy (J. Funct. Program., 1997)

A Computational Formalization for Partial Evaluation. - John Hatcliff; Olivier Danvy (Math. Struct. Comput. Sci., 1997)

Generalization in Hierarchies of Online Program Specialization Systems. - Robert Glück; John Hatcliff; Jesper Jørgensen (LOPSTR, 1998)

An Introduction to Online and Offline Partial Evaluation using a Simple Flowchart Language. - John Hatcliff (Partial Evaluation, 1998)

Staging Static Analyses Using Abstraction-Based Program Specialization. - John Hatcliff; Matthew B. Dwyer; Shawn Laubach (PLILP/ALP, 1998)

Using Partial Evaluation to Enable Verification of Concurrent Software. - Matthew B. Dwyer; John Hatcliff; Muhammad Nanda (ACM Comput. Surv., 1998)

Foundations for Partial Evaluation of Functional Programs with Computational Effects. - John Hatcliff (ACM Comput. Surv., 1998)

Slicing Software for Model Construction. - Matthew B. Dwyer; John Hatcliff (PEPM, 1999)

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 (SAS, 1999)

CPS Translations and Applications: The Cube and Beyond. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (High. Order Symb. Comput., 1999)

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 (ICSE, 2000)

Bandera: a source-level interface for model checking Java programs. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (ICSE, 2000)

A Language Framework for Expressing Checkable Properties of Dynamic Software. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (SPIN, 2000)

Slicing Software for Model Construction. - John Hatcliff; Matthew B. Dwyer; Hongjun Zheng (High. Order Symb. Comput., 2000)

Adapting programming languages technologies for finite-state verification. - Matthew B. Dwyer; John Hatcliff (ACM SIGSOFT Softw. Eng. Notes, 2000)

Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. - John Hatcliff; Matthew B. Dwyer (CONCUR, 2001)

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 (ICSE, 2001)

An induction principle for pure type systems. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (Theor. Comput. Sci., 2001)

Weak normalization implies strong normalization in a class of non-dependent pure type systems. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (Theor. Comput. Sci., 2001)

Foundations of the Bandera Abstraction Tools. - John Hatcliff; Matthew B. Dwyer; Corina S. Pasareanu; Robby (The Essence of Computation, 2002)

Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. - Xianghua Deng; Matthew B. Dwyer; John Hatcliff; Georg Jung; Robby; Gurdip Singh (FMCO, 2002)

Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. - Xianghua Deng; Matthew B. Dwyer; John Hatcliff; Masaaki Mizuno (ICSE, 2002)

Expressing checkable properties of dynamic systems: the Bandera Specification Language. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (Int. J. Softw. Tools Technol. Transf., 2002)

Space Reductions for Model Checking Quasi-Cyclic Systems. - Matthew B. Dwyer; Robby; Xianghua Deng; John Hatcliff (EMSOFT, 2003)

Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. - John Hatcliff; Xianghua Deng; Matthew B. Dwyer; Georg Jung; Venkatesh Prasad Ranganath (ICSE, 2003)

Cadena: enabling CCM-based application development in Eclipse. - Venkatesh Prasad Ranganath; Adam Childs; Jesse Greenwald; Matthew B. Dwyer; John Hatcliff; Gurdip Singh (eTX, 2003)

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 (PEPM, 2003)

Bogor: an extensible and highly-modular software model checking framework. - Robby; Matthew B. Dwyer; John Hatcliff (ESEC / SIGSOFT FSE, 2003)

Space-Reduction Strategies for Model Checking Dynamic Software. - Robby; Matthew B. Dwyer; John Hatcliff; Radu Iosif (SoftMC@CAV, 2003)

A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. - Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff; Robby (CASSIS, 2004)

Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. - Venkatesh Prasad Ranganath; John Hatcliff (CC, 2004)

Supporting model checking education using BOGOR/Eclipse. - Matthew B. Dwyer; John Hatcliff; Matthew Hoosier (eTX, 2004)

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 (FASE, 2004)

A Correlation Framework for the CORBA Component Model. - Georg Jung; John Hatcliff; Venkatesh Prasad Ranganath (FASE, 2004)

A Case Study in Domain-customized Model Checking for Real-time Component Software. - Matthew Hoosier; John Hatcliff; Robby; Matthew B. Dwyer (ISoLA (Preliminary proceedings), 2004)

SyncGen: An Aspect-Oriented Framework for Synchronization. - Xianghua Deng; Matthew B. Dwyer; John Hatcliff; Masaaki Mizuno (TACAS, 2004)

Checking Strong Specifications Using an Extensible Software Model Checking Framework. - Robby; Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff (TACAS, 2004)

Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. - John Hatcliff; Robby; Matthew B. Dwyer (VMCAI, 2004)

Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs. - Matthew B. Dwyer; John Hatcliff; Robby; Venkatesh Prasad Ranganath (Formal Methods Syst. Des., 2004)

An Integrated Model-Driven Development Environment for Composing and Validating Distributed Real-Time and Embedded Systems. - Gabriele Trombetti; Aniruddha Gokhale; Douglas C. Schmidt; Jesse Greenwald; John Hatcliff; Georg Jung; Gurdip Singh (Model-Driven Software Development, 2005)

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. - Matthew B. Dwyer; John Hatcliff; Matthew Hoosier; Robby (CAV, 2005)

Extending JML for Modular Specification and Verification of Multi-threaded Programs. - Edwin Rodríguez; Matthew B. Dwyer; Cormac Flanagan; John Hatcliff; Gary T. Leavens; Robby (ECOOP, 2005)

Kaveri: Delivering the Indus Java Program Slicer to Eclipse. - Ganeshan Jayaraman; Venkatesh Prasad Ranganath; John Hatcliff (FASE, 2005)

Translating Java for Multiple Model Checkers: The Bandera Back-End. - Radu Iosif; Matthew B. Dwyer; John Hatcliff (Formal Methods Syst. Des., 2005)

Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. - Xianghua Deng; Robby; John Hatcliff (ISoLA, 2006)

Domain-specific Model Checking Using The Bogor Framework. - Robby; Matthew B. Dwyer; John Hatcliff (ASE, 2006)

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 (TACAS, 2006)

Bogor: A Flexible Framework for Creating Software Model Checkers. - Robby; Matthew B. Dwyer; John Hatcliff (TAIC PART, 2006)

CALM and Cadena: Metamodeling for Component-Based Product-Line Development. - Adam Childs; Jesse Greenwald; Georg Jung; Matthew Hoosier; John Hatcliff (Computer, 2006)

High-Confidence Medical Device Software and Systems. - Insup Lee 001; George J. Pappas; Rance Cleaveland; John Hatcliff; Bruce H. Krogh; Peter Lee 001; Harvey Rubin; Lui Sha (Computer, 2006)

Introduction to special issue. - John Hatcliff; Insup Lee 001; Oleg Sokolsky (SIGBED Rev., 2006)

Towards highly optimized real-time middleware for software product-line architectures. - Arvind S. Krishna; Aniruddha S. Gokhale; Douglas C. Schmidt; Venkatesh Prasad Ranganath; John Hatcliff (SIGBED Rev., 2006)

PEPM 2006 paper abstracts. - Mark W. Bailey; John Hatcliff; Frank Tip (ACM SIGPLAN Notices, 2006)

Why you should definitely read this special section. - Hubert Garavel; John Hatcliff (Int. J. Softw. Tools Technol. Transf., 2006)

Checking JML specifications using an extensible software model checking framework. - Robby; Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff (Int. J. Softw. Tools Technol. Transf., 2006)

TACAS 2003 Special Issue - Preface. - Hubert Garavel; John Hatcliff (Theor. Comput. Sci., 2006)

Formal Software Analysis Emerging Trends in Software Model Checking. - Matthew B. Dwyer; John Hatcliff; Robby; Corina S. Pasareanu; Willem Visser (FOSE, 2007)

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. - Xianghua Deng; Robby; John Hatcliff (SEFM, 2007)

A correlation framework for the CORBA component model. - Georg Jung; John Hatcliff (Int. J. Softw. Tools Technol. Transf., 2007)

Slicing concurrent Java programs using Indus and Kaveri. - Venkatesh Prasad Ranganath; John Hatcliff (Int. J. Softw. Tools Technol. Transf., 2007)

A new foundation for control dependence and slicing for modern program structures. - Venkatesh Prasad Ranganath; Torben Amtoft; Anindya Banerjee 001; John Hatcliff; Matthew B. Dwyer (ACM Trans. Program. Lang. Syst., 2007)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (FM, 2008)

Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. - John Hatcliff (ICFEM, 2008)

A Software Certification Consortium and its Top 9 Hurdles. - John Hatcliff; Mats Per Erik Heimdahl; Mark Lawford; T. S. E. Maibaum; Alan Wassyng; Fred L. Wurden (SafeCert@ETAPS, 2008)

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 (ICSE Companion, 2009)

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 (ICSE Companion, 2009)

A publish-subscribe architecture and component-based programming model for medical device interoperability. - Andrew L. King; Sam Procter; Daniel Andresen; John Hatcliff; Steve Warren; William Spees; Raoul Praful Jetley; Paul L. Jones; Sandy Weininger (SIGBED Rev., 2009)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Software certification consortium: certification methods for safety-critical software. - Alan Wassyng; Mark Lawford; T. S. E. Maibaum; Jens H. Weber; John Hatcliff (CASCON, 2010)

Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. - Torben Amtoft; John Hatcliff; Edwin Rodríguez (ESOP, 2010)

Prototyping closed loop physiologic control with the medical device coordination framework. - Andrew L. King; David Arney; Insup Lee 001; Oleg Sokolsky; John Hatcliff; Sam Procter (SEHC@ICSE, 2010)

A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. - Georg Jung; John Hatcliff (Sci. Comput. Program., 2010)

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (NASA Formal Methods, 2011)

Enhancing spark's contract checking facilities using symbolic execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (SIGAda, 2011)

Rationale and Architecture Principles for Medical Application Platforms. - John Hatcliff; Andrew L. King; Insup Lee 001; Alasdair Macdonald; Anura Fernando; Michael Robkin; Eugene Y. Vasserman; Sandy Weininger; Julian M. Goldman (ICCPS, 2012)

Requirements specification for apps in medical application platforms. - Brian R. Larson; John Hatcliff; Sam Procter; Patrice Chalin (SEHC@ICSE, 2012)

Component-based app design for platform-oriented devices in a medical device coordination framework. - Kejia Li; Steve Warren; John Hatcliff (IHI, 2012)

Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. - Jason Belt; Robby; Patrice Chalin; John Hatcliff; Xianghua Deng (NASA Formal Methods, 2012)

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. - Torben Amtoft; Josiah Dodds; Zhi Zhang; Andrew W. Appel; Lennart Beringer; John Hatcliff; Xinming Ou; Andrew Cousino (POST, 2012)

Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. - Hariharan Thiagarajan; John Hatcliff; Jason Belt; Robby (SCAM, 2012)

Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. - Jason Belt; Patrice Chalin; John Hatcliff; Robby (HILT, 2012)

Behavioral interface specification languages. - John Hatcliff; Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001; Matthew J. Parkinson (ACM Comput. Surv., 2012)

Challenges and Research Directions in Medical Cyber-Physical Systems. - Insup Lee 001; Oleg Sokolsky; Sanjian Chen; John Hatcliff; Eunkyoung Jee; BaekGyu Kim; Andrew L. King; Margaret Mullen-Fortino; Soojin Park; Alex Roederer; Krishna K. Venkatasubramanian (Proc. IEEE, 2012)

Explicating symbolic execution (xSymExe): an evidence-based verification framework. - John Hatcliff; Robby; Patrice Chalin; Jason Belt (ICSE, 2013)

Open source patient-controlled analgesic pump requirements documentation. - Brian R. Larson; John Hatcliff; Patrice Chalin (SEHC@ICSE, 2013)

BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. - Brian R. Larson; Patrice Chalin; John Hatcliff (NASA Formal Methods, 2013)

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. - Pierre Courtieu; Maria-Virginia Aponte; Tristan Crolard; Zhi Zhang; Robby; Jason Belt; John Hatcliff; Jérôme Guitton; Trevor Jennings (HILT, 2013)

Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device. - Brian R. Larson; John Hatcliff; Kim R. Fowler; Julien Delange (HILT, 2013)

Foundational Security Principles for Medical Application Platforms - (Extended Abstract). - Eugene Y. Vasserman; John Hatcliff (WISA, 2013)

Software Certification: Methods and Tools (Dagstuhl Seminar 13051). - Darren D. Cofer; John Hatcliff; Michaela Huhn; Mark Lawford (Dagstuhl Reports, 2013)

Towards an AADL-Based Definition of App Architecture for Medical Application Platforms. - Sam Procter; John Hatcliff; Robby (FHIES/SEHC, 2014)

Certifiably safe software-dependent systems: challenges and directions. - John Hatcliff; Alan Wassyng; Tim Kelly; Cyrille Comar; Paul L. Jones (FOSE, 2014)

An architecturally-integrated, systems-based hazard analysis for medical applications. - Sam Procter; John Hatcliff (MEMOCODE, 2014)

Communication patterns for interconnecting and composing medical systems. - Venkatesh-Prasad Ranganath; Yu Jin Kim; John Hatcliff; Robby (EMBC, 2015)

Ecosphere Principles for Medical Application Platforms. - Yu Jin Kim; Sam Procter; John Hatcliff; Venkatesh-Prasad Ranganath; Robby (ICHI, 2015)

Towards Assurance for Plug & Play Medical Systems. - Andrew L. King; Lu Feng 001; Sam Procter; Sanjian Chen; Oleg Sokolsky; John Hatcliff; Insup Lee 001 (SAFECOMP, 2015)

Error Type Refinement for Assurance of Families of Platform-Based Systems. - Sam Procter; John Hatcliff; Sandy Weininger; Anura Fernando (SAFECOMP Workshops, 2015)

Enabling Safe Interoperation by Medical Device Virtual Integration. - Brian R. Larson; Yi Zhang 051; Stephen C. Barrett; John Hatcliff; Paul L. Jones (IEEE Des. Test, 2015)

SAFE and Secure: Deeply Integrating Security in a New Hazard Analysis. - Sam Procter; Eugene Y. Vasserman; John Hatcliff (ARES, 2017)

Enhanced Security of Building Automation Systems Through Microkernel-Based Controller Platforms. - Xiaolong Wang; Richard Habeeb; Xinming Ou; Siddharth Amaravadi; John Hatcliff; Masaaki Mizuno; Mitchell L. Neilsen; S. Raj Rajagopalan; Srivatsan Varadarajan (ICDCS Workshops, 2017)

Focused Certification of an Industrial Compilation and Static Verification Toolchain. - Zhi Zhang; Robby; John Hatcliff; Yannick Moy; Pierre Courtieu (SEFM, 2017)

A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices. - Todd Carpenter; John Hatcliff; Eugene Y. Vasserman (SafeThings@SenSys, 2017)

A Unified Approach for Modeling, Developing, and Assuring Critical Systems. - John Hatcliff; Brian R. Larson; Jason Belt; Robby; Yi Zhang 051 (ISoLA (1), 2018)

Model-Based Development for High-Assurance Embedded Systems. - Robby; John Hatcliff; Jason Belt (ISoLA (1), 2018)

Assurance Case Considerations for Interoperable Medical Systems. - Yi Zhang 051; Brian R. Larson; John Hatcliff (SAFECOMP Workshops, 2018)

The open PCA pump project: an exemplar open source medical device as a community resource. - John Hatcliff; Brian R. Larson; Todd Carpenter; Paul L. Jones; Yi Zhang 051; Joseph Jorgens (SIGBED Rev., 2019)

Model-Based Risk Analysis for an Open-Source PCA Pump Using AADL Error Modeling. - Hariharan Thiagarajan; Brian R. Larson; John Hatcliff; Yi Zhang 051 (IMBSA, 2020)

HAMR: An AADL Multi-platform Code Generation Toolset. - John Hatcliff; Jason Belt; Robby; Todd Carpenter (ISoLA, 2021)

Slang: The Sireum Programming Language. - Robby; John Hatcliff (ISoLA, 2021)

Formalization of the AADL Run-Time Services. - John Hatcliff; Jérôme Hugues; Danielle Stewart; Lutz Wrage (ISoLA (2), 2022)

Mechanization of a Large DSML: An Experiment with AADL and Coq. - Jérôme Hugues; Lutz Wrage; John Hatcliff; Danielle Stewart (MEMOCODE, 2022)

Cyberassured Systems Engineering at Scale. - 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 (IEEE Secur. Priv., 2022)

Awas: AADL information flow and error propagation analysis framework. - Hariharan Thiagarajan; John Hatcliff; Robby (Innov. Syst. Softw. Eng., 2022)

Specification and Verification of Timing Properties in Interoperable Medical Systems. - Mahsa Zarneshan; Fatemeh Ghassemi; Ehsan Khamespanah; Marjan Sirjani; John Hatcliff (Log. Methods Comput. Sci., 2022)

Model-driven development for the seL4 microkernel using the HAMR framework. - 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; et al. (J. Syst. Archit., 2023)

Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041). - Erika Ábrahám; Stefan Hallerstede; John Hatcliff; Danielle Stewart; Noah Abou El Wafa (Dagstuhl Reports, 2023)

Logika: The Sireum Verification Framework. - Robby; John Hatcliff; Jason Belt (FMICS, 2024)

Integrated Contract-Based Unit and System Testing for Component-Based Systems. - John Hatcliff; Jason Belt; Robby; David S. Hardin (NFM, 2024)

Teaching with Logika: Conceiving and Constructing Correct Software. - Stefan Hallerstede; John Hatcliff; Robby (FMTea, 2024)

The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering. - John Hatcliff; Jason Belt (The Combined Power of Research, Education, and Dissemination, 2025)

Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. - Stefan Hallerstede; Robby; John Hatcliff; Jason Belt; David S. Hardin (FMICS, 2025)

End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR. - John Hatcliff; Jason Belt; Robby; Clint McKenzie; Catalina Liang (FMICS, 2025)

A mechanized semantics for component-based systems in the HAMR AADL runtime. - Stefan Hallerstede; John Hatcliff (Sci. Comput. Program., 2025)

Automated property-based testing from AADL component contracts. - John Hatcliff; Jason Belt; Robby; Jacob Legg; Danielle Stewart; Todd Carpenter (Int. J. Softw. Tools Technol. Transf., 2025)