A mechanized semantics for component-based systems in the HAMR AADL runtime.

John Hatcliff Kansas State Uniersity, Manhattan, KS, USA https://www.cs.ksu.edu/about/people/faculty/hatcliff/ https://scholar.google.com/citations?user=B56JLs0AAAAJ

Stefan Hallerstede John Hatcliff A mechanized semantics for component-based systems in the HAMR AADL runtime. 103312 2025 245 Sci. Comput. Program. https://doi.org/10.1016/j.scico.2025.103312 db/journals/scp/scp245.html#HallerstedeH25 streams/journals/scp

John Hatcliff Jason Belt Robby Jacob Legg Danielle Stewart Todd Carpenter Automated property-based testing from AADL component contracts. 333-360 2025 June 27 Int. J. Softw. Tools Technol. Transf. 3 https://doi.org/10.1007/s10009-025-00792-3 db/journals/sttt/sttt27.html#HatcliffBRLSC25 streams/journals/sttt

Robby John Hatcliff Jason Belt Logika: the Sireum verification framework. 487-510 2025 October 27 Int. J. Softw. Tools Technol. Transf. 5 https://doi.org/10.1007/s10009-025-00828-8 db/journals/sttt/sttt27.html#RobbyHB25 streams/journals/sttt

John Hatcliff Jason Belt The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering. 93-117 2025 The Combined Power of Research, Education, and Dissemination https://doi.org/10.1007/978-3-031-73887-6_9 conf/birthday/2025margaria db/conf/birthday/margaria2025.html#HatcliffB25 Stefan Hallerstede Robby John Hatcliff Jason Belt David S. Hardin Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. 39-58 2025 FMICS https://doi.org/10.1007/978-3-032-00942-5_3 conf/fmics/2025 db/conf/fmics/fmics2025.html#HallerstedeRHBH25 streams/conf/fmics John Hatcliff Jason Belt Robby Clint McKenzie Catalina Liang End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR. 241-260 2025 FMICS https://doi.org/10.1007/978-3-032-00942-5_13 conf/fmics/2025 db/conf/fmics/fmics2025.html#HatcliffBRML25 streams/conf/fmics Robby John Hatcliff Jason Belt Logika: The Sireum Verification Framework. 97-116 2024 FMICS https://doi.org/10.1007/978-3-031-68150-9_6 conf/fmics/2024 db/conf/fmics/fmics2024.html#RobbyHB24 streams/conf/fmics John Hatcliff Jason Belt Robby David S. Hardin Integrated Contract-Based Unit and System Testing for Component-Based Systems. 406-426 2024 NFM https://doi.org/10.1007/978-3-031-60698-4_25 conf/nfm/2024 db/conf/nfm/nfm2024.html#HatcliffBRH24 Stefan Hallerstede John Hatcliff Robby Teaching with Logika: Conceiving and Constructing Correct Software. 106-123 2024 FMTea https://doi.org/10.1007/978-3-031-71379-8_7 conf/tfm/2024 db/conf/tfm/fmtea2024.html#HallerstedeHR24 streams/conf/tfm

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. 102789 2023 134 J. Syst. Archit. https://doi.org/10.1016/j.sysarc.2022.102789 db/journals/jsa/jsa134.html#BeltHRSCCMABCHH23

Stefan Hallerstede John Hatcliff A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime. 45-64 2023 FACS https://doi.org/10.1007/978-3-031-52183-6_3 conf/facs2/2023 db/conf/facs2/facs2023.html#HallerstedeH23 John Hatcliff Jason Belt Robby Jacob Legg Danielle Stewart Todd Carpenter Automated Property-Based Testing from AADL Component Contracts. 131-150 2023 FMICS https://doi.org/10.1007/978-3-031-43681-9_8 conf/fmics/2023 db/conf/fmics/fmics2023.html#HatcliffBRLSC23

Erika Ábrahám Stefan Hallerstede John Hatcliff Danielle Stewart Noah Abou El Wafa Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041). 155-183 2023 January 13 Dagstuhl Reports 1 https://doi.org/10.4230/DagRep.13.1.155 db/journals/dagstuhl-reports/dagstuhl-reports13.html#AbrahamHHSW23

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. 52-64 2022 20 IEEE Secur. Priv. 3 https://doi.org/10.1109/MSEC.2022.3151733 db/journals/ieeesp/ieeesp20.html#CoferABHSAHRKLM22

Hariharan Thiagarajan John Hatcliff Robby Awas: AADL information flow and error propagation analysis framework. 485-504 2022 18 Innov. Syst. Softw. Eng. 4 https://doi.org/10.1007/s11334-021-00410-w db/journals/isse/isse18.html#ThiagarajanHR22

Mahsa Zarneshan Fatemeh Ghassemi Ehsan Khamespanah Marjan Sirjani John Hatcliff Specification and Verification of Timing Properties in Interoperable Medical Systems. 2022 18 Log. Methods Comput. Sci. 2 https://doi.org/10.46298/lmcs-18(2:13)2022 db/journals/lmcs/lmcs18.html#ZarneshanGKSH22

John Hatcliff Jérôme Hugues Danielle Stewart Lutz Wrage Formalization of the AADL Run-Time Services. 105-134 2022 ISoLA (2) https://doi.org/10.1007/978-3-031-19756-7_7 conf/isola/2022-2 db/conf/isola/isola2022-2.html#HatcliffHSW22 Jérôme Hugues Lutz Wrage John Hatcliff Danielle Stewart Mechanization of a Large DSML: An Experiment with AADL and Coq. 1-9 2022 MEMOCODE https://doi.org/10.1109/MEMOCODE57689.2022.9954589 conf/memocode/2022 db/conf/memocode/memocode2022.html#HuguesWHS22 Robby John Hatcliff Slang: The Sireum Programming Language. 253-273 2021 ISoLA https://doi.org/10.1007/978-3-030-89159-6_17 conf/isola/2021 db/conf/isola/isola2021.html#RobbyH21 John Hatcliff Jason Belt Robby Todd Carpenter HAMR: An AADL Multi-platform Code Generation Toolset. 274-295 2021 ISoLA https://doi.org/10.1007/978-3-030-89159-6_18 conf/isola/2021 db/conf/isola/isola2021.html#HatcliffBRC21 Hariharan Thiagarajan John Hatcliff Robby Awas: AADL Information Flow and Error Propagation Analysis Framework. 294-310 2020 ECSA Companion https://doi.org/10.1007/978-3-030-59155-7_23 conf/ecsa/2020c db/conf/ecsa/ecsa2020c.html#ThiagarajanHR20 Hariharan Thiagarajan Brian R. Larson John Hatcliff Yi Zhang 0051 Model-Based Risk Analysis for an Open-Source PCA Pump Using AADL Error Modeling. 34-50 2020 IMBSA https://doi.org/10.1007/978-3-030-58920-2_3 conf/imbsa/2020 db/conf/imbsa/imbsa2020.html#ThiagarajanLHZ20

Mahsa Zarneshan Fatemeh Ghassemi Ehsan Khamespanah Marjan Sirjani John Hatcliff Specification and Verification of Timing Properties in Interoperable Medical Systems. 2020 abs/2012.04025 CoRR https://arxiv.org/abs/2012.04025 db/journals/corr/corr2012.html#abs-2012-04025

John Hatcliff Brian R. Larson Todd Carpenter Paul L. Jones Yi Zhang 0051 Joseph Jorgens The open PCA pump project: an exemplar open source medical device as a community resource. 8-13 2019 16 SIGBED Rev. 2 https://doi.org/10.1145/3357495.3357496 https://www.wikidata.org/entity/Q114976924 db/journals/sigbed/sigbed16.html#HatcliffLCJZJ19

John Hatcliff Brian R. Larson Jason Belt Robby Yi Zhang 0051 A Unified Approach for Modeling, Developing, and Assuring Critical Systems. 225-245 2018 ISoLA (1) https://doi.org/10.1007/978-3-030-03418-4_14 conf/isola/2018-1 db/conf/isola/isola2018-1.html#HatcliffLBRZ18 Robby John Hatcliff Jason Belt Model-Based Development for High-Assurance Embedded Systems. 539-545 2018 ISoLA (1) https://doi.org/10.1007/978-3-030-03418-4_32 conf/isola/2018-1 db/conf/isola/isola2018-1.html#RobbyHB18 Yi Zhang 0051 Brian R. Larson John Hatcliff Assurance Case Considerations for Interoperable Medical Systems. 42-48 2018 SAFECOMP Workshops https://doi.org/10.1007/978-3-319-99229-7_5 conf/safecomp/2018w db/conf/safecomp/safecomp2018w.html#ZhangLH18 Sam Procter Eugene Y. Vasserman John Hatcliff SAFE and Secure: Deeply Integrating Security in a New Hazard Analysis. 66:1-66:10 2017 ARES https://doi.org/10.1145/3098954.3105823 conf/IEEEares/2017 db/conf/IEEEares/ares2017.html#ProcterVH17 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. 37-44 2017 ICDCS Workshops https://doi.org/10.1109/ICDCSW.2017.25 https://doi.ieeecomputersociety.org/10.1109/ICDCSW.2017.25 conf/icdcsw/2017 db/conf/icdcsw/icdcsw2017.html#WangHOAHMNRV17 Zhi Zhang Robby John Hatcliff Yannick Moy Pierre Courtieu Focused Certification of an Industrial Compilation and Static Verification Toolchain. 17-34 2017 SEFM https://doi.org/10.1007/978-3-319-66197-1_2 conf/sefm/2017 db/conf/sefm/sefm2017.html#ZhangRHMC17 Todd Carpenter John Hatcliff Eugene Y. Vasserman A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices. 14-19 2017 SafeThings@SenSys https://doi.org/10.1145/3137003.3137008 conf/sensys/2017safethings db/conf/sensys/safethings2017.html#CarpenterHV17

Brian R. Larson Yi Zhang 0051 Stephen C. Barrett John Hatcliff Paul L. Jones Enabling Safe Interoperation by Medical Device Virtual Integration. 74-88 2015 32 IEEE Des. Test 5 https://doi.org/10.1109/MDAT.2015.2464813 db/journals/dt/dt32.html#LarsonZBHJ15

Venkatesh-Prasad Ranganath Yu Jin Kim John Hatcliff Robby Communication patterns for interconnecting and composing medical systems. 1711-1716 2015 EMBC https://doi.org/10.1109/EMBC.2015.7318707 https://www.wikidata.org/entity/Q51574664 conf/embc/2015 db/conf/embc/embc2015.html#RanganathKHR15 Yu Jin Kim Sam Procter John Hatcliff Venkatesh-Prasad Ranganath Robby Ecosphere Principles for Medical Application Platforms. 193-198 2015 ICHI https://doi.org/10.1109/ICHI.2015.30 https://doi.ieeecomputersociety.org/10.1109/ICHI.2015.30 conf/ichi/2015 db/conf/ichi/ichi2015.html#KimPHRR15 Sam Procter John Hatcliff Sandy Weininger Anura Fernando Error Type Refinement for Assurance of Families of Platform-Based Systems. 95-106 2015 SAFECOMP Workshops https://doi.org/10.1007/978-3-319-24249-1_9 conf/safecomp/2015w db/conf/safecomp/safecomp2015w.html#ProcterHWF15 Andrew L. King Lu Feng 0001 Sam Procter Sanjian Chen Oleg Sokolsky John Hatcliff Insup Lee 0001 Towards Assurance for Plug & Play Medical Systems. 228-242 2015 SAFECOMP https://doi.org/10.1007/978-3-319-24255-2_17 conf/safecomp/2015 db/conf/safecomp/safecomp2015.html#KingFPCSHL15 Sam Procter John Hatcliff Robby Towards an AADL-Based Definition of App Architecture for Medical Application Platforms. 26-43 2014 FHIES/SEHC https://doi.org/10.1007/978-3-319-63194-3_3 conf/fhies/2014 db/conf/fhies/fhies2014.html#ProcterHR14 John Hatcliff Alan Wassyng Tim Kelly Cyrille Comar Paul L. Jones Certifiably safe software-dependent systems: challenges and directions. 182-200 2014 FOSE https://doi.org/10.1145/2593882.2593895 conf/icse/2014fose db/conf/icse/fose2014.html#HatcliffWKCJ14 Sam Procter John Hatcliff An architecturally-integrated, systems-based hazard analysis for medical applications. 124-133 2014 MEMOCODE https://doi.org/10.1109/MEMCOD.2014.6961850 conf/memocode/2014 db/conf/memocode/memocode2014.html#ProcterH14 Brian R. Larson John Hatcliff Patrice Chalin Open source patient-controlled analgesic pump requirements documentation. 28-34 2013 SEHC@ICSE https://doi.org/10.1109/SEHC.2013.6602474 https://doi.ieeecomputersociety.org/10.1109/SEHC.2013.6602474 http://dl.acm.org/citation.cfm?id=2663583 https://www.wikidata.org/entity/Q88084554 conf/icse/2013sehc db/conf/icse/sehc2013.html#LarsonHC13 John Hatcliff Robby Patrice Chalin Jason Belt Explicating symbolic execution (xSymExe): an evidence-based verification framework. 222-231 2013 ICSE https://doi.org/10.1109/ICSE.2013.6606568 https://doi.ieeecomputersociety.org/10.1109/ICSE.2013.6606568 http://dl.acm.org/citation.cfm?id=2486818 conf/icse/2013 db/conf/icse/icse2013.html#HatcliffRCB13 Brian R. Larson Patrice Chalin John Hatcliff BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. 276-290 2013 NASA Formal Methods https://doi.org/10.1007/978-3-642-38088-4_19 conf/nfm/2013 db/conf/nfm/nfm2013.html#LarsonCH13 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. 21-22 2013 HILT https://doi.org/10.1145/2527269.2527278 https://www.wikidata.org/entity/Q131114266 conf/sigada/2013 db/conf/sigada/hilt2013.html#CourtieuACZRBHG13 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. 65-84 2013 HILT https://doi.org/10.1145/2527269.2527271 https://www.wikidata.org/entity/Q130976182 conf/sigada/2013 db/conf/sigada/hilt2013.html#LarsonHFD13 Eugene Y. Vasserman John Hatcliff Foundational Security Principles for Medical Application Platforms - (Extended Abstract). 213-217 2013 WISA https://doi.org/10.1007/978-3-319-05149-9_13 https://www.wikidata.org/entity/Q86553887 conf/wisa/2013 db/conf/wisa/wisa2013.html#VassermanH13 Anindya Banerjee 0001 Olivier Danvy Kyung-Goo Doh John Hatcliff Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013. Festschrift for Dave Schmidt 2013 EPTCS https://doi.org/10.4204/EPTCS.129 http://arxiv.org/abs/1309.4557 129 db/series/eptcs/eptcs129.html

Darren D. Cofer John Hatcliff Michaela Huhn Mark Lawford Software Certification: Methods and Tools (Dagstuhl Seminar 13051). 111-148 2013 3 Dagstuhl Reports 1 https://doi.org/10.4230/DagRep.3.1.111 db/journals/dagstuhl-reports/dagstuhl-reports3.html#CoferHHL13

John Hatcliff Gary T. Leavens K. Rustan M. Leino Peter Müller 0001 Matthew J. Parkinson Behavioral interface specification languages. 16:1-16:58 2012 44 ACM Comput. Surv. 3 https://doi.org/10.1145/2187671.2187678 https://www.wikidata.org/entity/Q131117441 db/journals/csur/csur44.html#HatcliffLLMP12

Insup Lee 0001 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. 75-90 2012 100 Proc. IEEE 1 https://doi.org/10.1109/JPROC.2011.2165270 db/journals/pieee/pieee100.html#LeeSCHJKKMPRV12

John Hatcliff Andrew L. King Insup Lee 0001 Alasdair Macdonald Anura Fernando Michael Robkin Eugene Y. Vasserman Sandy Weininger Julian M. Goldman Rationale and Architecture Principles for Medical Application Platforms. 3-12 2012 ICCPS https://doi.org/10.1109/ICCPS.2012.9 https://doi.ieeecomputersociety.org/10.1109/ICCPS.2012.9 conf/iccps/2012 db/conf/iccps/iccps2012.html#HatcliffKLMFRVWG12 Brian R. Larson John Hatcliff Sam Procter Patrice Chalin Requirements specification for apps in medical application platforms. 26-32 2012 SEHC@ICSE https://doi.org/10.1109/SEHC.2012.6227013 http://dl.acm.org/citation.cfm?id=2667041 conf/icse/2012sehc db/conf/icse/sehc2012.html#LarsonHPC12 Kejia Li Steve Warren John Hatcliff Component-based app design for platform-oriented devices in a medical device coordination framework. 343-352 2012 IHI https://doi.org/10.1145/2110363.2110403 https://www.wikidata.org/entity/Q130977399 conf/ihi/2012 db/conf/ihi/ihi2012.html#LiWH12 Jason Belt Robby Patrice Chalin John Hatcliff Xianghua Deng Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. 295-309 2012 NASA Formal Methods https://doi.org/10.1007/978-3-642-28891-3_29 conf/nfm/2012 db/conf/nfm/nfm2012.html#BeltRCHD12 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. 369-389 2012 POST https://doi.org/10.1007/978-3-642-28641-4_20 conf/post/2012 db/conf/post/post2012.html#AmtoftDZABHOC12 Hariharan Thiagarajan John Hatcliff Jason Belt Robby Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. 132-137 2012 SCAM https://doi.org/10.1109/SCAM.2012.25 https://doi.ieeecomputersociety.org/10.1109/SCAM.2012.25 conf/scam/2012 db/conf/scam/scam2012.html#ThiagarajanHBR12 Jason Belt Patrice Chalin John Hatcliff Robby Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. 3-4 2012 HILT https://doi.org/10.1145/2402676.2402679 https://www.wikidata.org/entity/Q131116115 conf/sigada/2012 db/conf/sigada/hilt2012.html#BeltCHR12 Ruth Breu John Hatcliff Proceedings of the 4th International Workshop on Software Engineering in Health Care, SEHC 2012, Zurich, Switzerland, June 4-5, 2012 SEHC@ICSE IEEE Computer Society 2012 978-1-4673-1843-3 https://ieeexplore.ieee.org/xpl/conhome/6218998/proceeding http://www.computer.org/csdl/proceedings/sehc/2012/1844/00/index.html http://dl.acm.org/citation.cfm?id=2667036 db/conf/icse/sehc2012.html Jason Belt John Hatcliff Robby Patrice Chalin David S. Hardin Xianghua Deng Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. 58-72 2011 NASA Formal Methods https://doi.org/10.1007/978-3-642-20398-5_6 conf/nfm/2011 db/conf/nfm/nfm2011.html#BeltHRCHD11 Jason Belt John Hatcliff Robby Patrice Chalin David S. Hardin Xianghua Deng Enhancing spark's contract checking facilities using symbolic execution. 47-60 2011 SIGAda https://doi.org/10.1145/2070337.2070357 https://www.wikidata.org/entity/Q131114225 conf/sigada/2011 db/conf/sigada/sigada2011.html#BeltHRCHD11

Georg Jung John Hatcliff A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. 615-637 2010 75 Sci. Comput. Program. 7 https://doi.org/10.1016/j.scico.2009.12.008 db/journals/scp/scp75.html#JungH10

Alan Wassyng Mark Lawford T. S. E. Maibaum Jens H. Weber John Hatcliff Software certification consortium: certification methods for safety-critical software. 434-436 2010 CASCON https://doi.org/10.1145/1923947.1924033 conf/cascon/2010 db/conf/cascon/cascon2010.html#WassyngLMWH10 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. 43-63 2010 ESOP https://doi.org/10.1007/978-3-642-11957-6_4 conf/esop/2010 db/conf/esop/esop2010.html#AmtoftHR10 Andrew L. King David Arney Insup Lee 0001 Oleg Sokolsky John Hatcliff Sam Procter Prototyping closed loop physiologic control with the medical device coordination framework. 1-11 2010 SEHC@ICSE https://doi.org/10.1145/1809085.1809086 conf/icse/2010sehc db/conf/icse/sehc2010.html#KingALSHP10 Torben Amtoft John Hatcliff Edwin Rodríguez Robby Jonathan Hoag David A. Greve Specification and Checking of Software Contracts for Conditional Information Flow. 341-379 2010 Design and Verification of Microprocessor Systems for High-Assurance Applications https://doi.org/10.1007/978-1-4419-1539-9_12 books/sp/2010H db/books/collections/H2010.html#AmtoftHRRHG10 John Hatcliff Elena Zucca Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 International Conference, FORTE 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings 6117 2010 https://doi.org/10.1007/978-3-642-13464-7 https://www.wikidata.org/entity/Q56501637 978-3-642-13463-0 FMOODS/FORTE Lecture Notes in Computer Science Springer db/conf/forte/forte2010.html

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. 7 2009 6 SIGBED Rev. 2 https://doi.org/10.1145/1859823.1859830 db/journals/sigbed/sigbed6.html#KingPAHWSJJW09

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. 141-151 2009 ICSE Companion https://doi.org/10.1109/ICSE-COMPANION.2009.5070972 https://doi.ieeecomputersociety.org/10.1109/ICSE-COMPANION.2009.5070972 conf/icse/2009c db/conf/icse/icse2009c.html#KingPAHWSJJW09 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. 433-434 2009 ICSE Companion https://doi.org/10.1109/ICSE-COMPANION.2009.5071048 https://doi.ieeecomputersociety.org/10.1109/ICSE-COMPANION.2009.5071048 conf/icse/2009c db/conf/icse/icse2009c.html#KingPAHWSJJW09a Torben Amtoft John Hatcliff Edwin Rodríguez Robby Jonathan Hoag David A. Greve Specification and Checking of Software Contracts for Conditional Information Flow. 229-245 2008 FM https://doi.org/10.1007/978-3-540-68237-0_17 conf/fm/2008 db/conf/fm/fm2008.html#AmtoftHRRHG08 John Hatcliff Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. 3-4 2008 ICFEM https://doi.org/10.1007/978-3-540-88194-0_3 conf/icfem/2008 db/conf/icfem/icfem2008.html#Hatcliff08 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. 11-17 2008 conf/safecert/2008 SafeCert@ETAPS https://doi.org/10.1016/j.entcs.2009.09.002 db/conf/safecert/safecert2008.html#HatcliffHLMWW09

Georg Jung John Hatcliff A correlation framework for the CORBA component model. 417-427 2007 9 Int. J. Softw. Tools Technol. Transf. 5-6 https://doi.org/10.1007/s10009-007-0041-2 db/journals/sttt/sttt9.html#JungH07

Venkatesh Prasad Ranganath John Hatcliff Slicing concurrent Java programs using Indus and Kaveri. 489-504 2007 9 Int. J. Softw. Tools Technol. Transf. 5-6 https://doi.org/10.1007/s10009-007-0043-0 db/journals/sttt/sttt9.html#RanganathH07

Venkatesh Prasad Ranganath Torben Amtoft Anindya Banerjee 0001 John Hatcliff Matthew B. Dwyer A new foundation for control dependence and slicing for modern program structures. 2007 29 ACM Trans. Program. Lang. Syst. 5 https://doi.org/10.1145/1275497.1275502 db/journals/toplas/toplas29.html#RanganathABHD07 27

Georg Jung John Hatcliff A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. 33-42 2007 GPCE https://doi.org/10.1145/1289971.1289979 conf/gpce/2007 db/conf/gpce/gpce2007.html#JungH07 Matthew B. Dwyer John Hatcliff Robby Corina S. Pasareanu Willem Visser Formal Software Analysis Emerging Trends in Software Model Checking. 120-136 2007 FOSE https://doi.org/10.1109/FOSE.2007.6 https://doi.ieeecomputersociety.org/10.1109/FOSE.2007.6 http://dl.acm.org/citation.cfm?id=1254714 conf/icse/2007fose db/conf/icse/fose2007.html#DwyerHRPV07 Xianghua Deng Robby John Hatcliff Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. 273-282 2007 conf/sefm/2007 SEFM https://doi.org/10.1109/SEFM.2007.43 https://doi.ieeecomputersociety.org/10.1109/SEFM.2007.43 db/conf/sefm/sefm2007.html#DengRH07

Adam Childs Jesse Greenwald Georg Jung Matthew Hoosier John Hatcliff CALM and Cadena: Metamodeling for Component-Based Product-Line Development. 42-50 2006 39 Computer 2 https://doi.org/10.1109/MC.2006.51 http://doi.ieeecomputersociety.org/10.1109/MC.2006.51 db/journals/computer/computer39.html#ChildsGJHH06

Insup Lee 0001 George J. Pappas Rance Cleaveland John Hatcliff Bruce H. Krogh Peter Lee 0001 Harvey Rubin Lui Sha High-Confidence Medical Device Software and Systems. 33-38 2006 39 Computer 4 https://doi.org/10.1109/MC.2006.127 http://doi.ieeecomputersociety.org/10.1109/MC.2006.127 https://www.wikidata.org/entity/Q57582024 db/journals/computer/computer39.html#LeePCHKLRS06

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. 13-16 2006 3 SIGBED Rev. 1 https://doi.org/10.1145/1279711.1279715 db/journals/sigbed/sigbed3.html#KrishnaGSRH06

John Hatcliff Insup Lee 0001 Oleg Sokolsky Introduction to special issue. 2006 3 SIGBED Rev. 4 https://doi.org/10.1145/1183088.1183089 db/journals/sigbed/sigbed3.html#HatcliffLS06

Mark W. Bailey John Hatcliff Frank Tip PEPM 2006 paper abstracts. 4-8 2006 41 ACM SIGPLAN Notices 3 https://doi.org/10.1145/1140543.1140545 db/journals/sigplan/sigplan41.html#BaileyHT06

Hubert Garavel John Hatcliff Why you should definitely read this special section. 1-3 2006 8 Int. J. Softw. Tools Technol. Transf. 1 https://doi.org/10.1007/s10009-005-0199-4 db/journals/sttt/sttt8.html#GaravelH06

Robby Edwin Rodríguez Matthew B. Dwyer John Hatcliff Checking JML specifications using an extensible software model checking framework. 280-299 2006 8 Int. J. Softw. Tools Technol. Transf. 3 https://doi.org/10.1007/s10009-005-0218-5 db/journals/sttt/sttt8.html#RobbyRDH06

Hubert Garavel John Hatcliff TACAS 2003 Special Issue - Preface. 169-172 2006 354 Theor. Comput. Sci. 2 https://doi.org/10.1016/j.tcs.2005.11.014 db/journals/tcs/tcs354.html#GaravelH06

Xianghua Deng Robby John Hatcliff Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. 137 2006 ISoLA https://doi.org/10.1109/ISoLA.2006.60 https://doi.ieeecomputersociety.org/10.1109/ISoLA.2006.60 conf/isola/2006 db/conf/isola/isola2006.html#DengRH06 Robby Matthew B. Dwyer John Hatcliff Domain-specific Model Checking Using The Bogor Framework. 369-370 2006 conf/kbse/2006 ASE https://doi.org/10.1109/ASE.2006.34 https://doi.ieeecomputersociety.org/10.1109/ASE.2006.34 db/conf/kbse/ase2006.html#RobbyDH06 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. 73-89 2006 conf/tacas/2006 TACAS https://doi.org/10.1007/11691372_5 db/conf/tacas/tacas2006.html#DwyerHHRRW06 Robby Matthew B. Dwyer John Hatcliff Bogor: A Flexible Framework for Creating Software Model Checkers. 3-22 2006 conf/taicpart/2006 TAIC PART https://doi.org/10.1109/TAIC-PART.2006.5 https://doi.ieeecomputersociety.org/10.1109/TAIC-PART.2006.5 db/conf/taicpart/taicpart2006.html#RobbyDH06 John Hatcliff Frank Tip Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2006, Charleston, South Carolina, USA, January 9-10, 2006 PEPM ACM 2006 1-59593-196-1 db/conf/pepm/pepm2006.html http://dl.acm.org/citation.cfm?id=1111542

Radu Iosif Matthew B. Dwyer John Hatcliff Translating Java for Multiple Model Checkers: The Bandera Back-End. 137-180 2005 26 Formal Methods Syst. Des. 2 https://doi.org/10.1007/s10703-005-1491-3 db/journals/fmsd/fmsd26.html#IosifDH05

Matthew B. Dwyer John Hatcliff Matthew Hoosier Robby Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. 148-152 2005 conf/cav/2005 CAV https://doi.org/10.1007/11513988_15 db/conf/cav/cav2005.html#DwyerHHR05 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. 551-576 2005 conf/ecoop/2005 ECOOP https://doi.org/10.1007/11531142_24 db/conf/ecoop/ecoop2005.html#RodriguezDFHLR05 Venkatesh Prasad Ranganath Torben Amtoft Anindya Banerjee 0001 Matthew B. Dwyer John Hatcliff A New Foundation for Control-Dependence and Slicing for Modern Program Structures. 77-93 https://doi.org/10.1007/978-3-540-31987-0_7 2005 conf/esop/2005 ESOP db/conf/esop/esop2005.html#RanganathABDH05 Ganeshan Jayaraman Venkatesh Prasad Ranganath John Hatcliff Kaveri: Delivering the Indus Java Program Slicer to Eclipse. 269-272 https://doi.org/10.1007/978-3-540-31984-9_20 2005 conf/fase/2005 FASE db/conf/fase/fase2005.html#JayaramanRH05 Gabriele Trombetti Aniruddha Gokhale Douglas C. Schmidt Jesse Greenwald John Hatcliff Georg Jung Gurdip Singh An Integrated Model-Driven Development Environment for Composing and Validating Distributed Real-Time and Embedded Systems. 329-361 2005 Model-Driven Software Development https://doi.org/10.1007/3-540-28554-7_15 books/sp/05/BBG2005 db/books/collections/BBG2005.html#TrombettiGSGHJS05

Matthew B. Dwyer John Hatcliff Robby Venkatesh Prasad Ranganath Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs. 199-240 2004 25 Formal Methods Syst. Des. 2-3 https://doi.org/10.1023/B:FORM.0000040028.49845.67 db/journals/fmsd/fmsd25.html#DwyerHRR04

Edwin Rodríguez Matthew B. Dwyer John Hatcliff Robby A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. 210-228 https://doi.org/10.1007/978-3-540-30569-9_11 2004 conf/cassis/2004 CASSIS db/conf/cassis/cassis2004.html#RodriguezDHR04 Venkatesh Prasad Ranganath John Hatcliff Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. 39-56 https://doi.org/10.1007/978-3-540-24723-4_4 2004 conf/cc/2004 CC db/conf/cc/cc2004.html#RanganathH04 Matthew B. Dwyer John Hatcliff Matthew Hoosier Supporting model checking education using BOGOR/Eclipse. 88-92 2004 eTX https://doi.org/10.1145/1066129.1066147 conf/eclipse/2004 db/conf/eclipse/eclipse2004.html#DwyerHH04 Georg Jung John Hatcliff Venkatesh Prasad Ranganath A Correlation Framework for the CORBA Component Model. 144-159 https://doi.org/10.1007/978-3-540-24721-0_10 2004 conf/fase/2004 FASE db/conf/fase/fase2004.html#JungHR04 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. 160-164 https://doi.org/10.1007/978-3-540-24721-0_11 2004 conf/fase/2004 FASE db/conf/fase/fase2004.html#ChildsGRDDHJSS04 Matthew Hoosier Matthew B. Dwyer Robby John Hatcliff A Case Study in Domain-Customized Model Checking for Real-Time Component Software. 161-180 2004 conf/isola/2004 ISoLA https://doi.org/10.1007/11925040_11 db/conf/isola/isola2004.html#HoosierDRH04 Matthew Hoosier John Hatcliff Robby Matthew B. Dwyer A Case Study in Domain-customized Model Checking for Real-time Component Software. 261-267 2004 ISoLA (Preliminary proceedings) conf/isola/2004i db/conf/isola/isola2004i.html#HoosierHRD04 Xianghua Deng Matthew B. Dwyer John Hatcliff Masaaki Mizuno SyncGen: An Aspect-Oriented Framework for Synchronization. 158-162 https://doi.org/10.1007/978-3-540-24730-2_13 2004 conf/tacas/2004 TACAS db/conf/tacas/tacas2004.html#DengDHM04 Robby Edwin Rodríguez Matthew B. Dwyer John Hatcliff Checking Strong Specifications Using an Extensible Software Model Checking Framework. 404-420 https://doi.org/10.1007/978-3-540-24730-2_31 2004 conf/tacas/2004 TACAS db/conf/tacas/tacas2004.html#RobbyRDH04 John Hatcliff Robby Matthew B. Dwyer Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. 175-190 https://doi.org/10.1007/978-3-540-24622-0_16 2004 conf/vmcai/2004 VMCAI db/conf/vmcai/vmcai2004.html#HatcliffRD04 Matthew B. Dwyer Robby Xianghua Deng John Hatcliff Space Reductions for Model Checking Quasi-Cyclic Systems. 173-189 https://doi.org/10.1007/978-3-540-45212-6_12 2003 conf/emsoft/2003 EMSOFT db/conf/emsoft/emsoft2003.html#DwyerRDH03 John Hatcliff Xianghua Deng Matthew B. Dwyer Georg Jung Venkatesh Prasad Ranganath Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. 160-173 2003 conf/icse/2003 ICSE https://doi.org/10.1109/ICSE.2003.1201197 https://doi.ieeecomputersociety.org/10.1109/ICSE.2003.1201197 http://dl.acm.org/citation.cfm?id=776836 db/conf/icse/icse2003.html#HatcliffDDJR03 Venkatesh Prasad Ranganath Adam Childs Jesse Greenwald Matthew B. Dwyer John Hatcliff Gurdip Singh Cadena: enabling CCM-based application development in Eclipse. 20-24 2003 conf/oopsla/2003ecl eTX https://doi.org/10.1145/965660.965665 db/conf/oopsla/oopsla2003ecl.html#RanganathCGDHS03 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. 1-2 2003 conf/pepm/2003 PEPM https://doi.org/10.1145/777388.777389 https://doi.org/10.1145/966049.777389 db/conf/pepm/pepm2003.html#HatcliffDDJRR03 Robby Matthew B. Dwyer John Hatcliff Bogor: an extensible and highly-modular software model checking framework. 267-276 2003 conf/sigsoft/2003 ESEC / SIGSOFT FSE https://doi.org/10.1145/940071.940107 db/conf/sigsoft/fse2003.html#RobbyDH03 Robby Matthew B. Dwyer John Hatcliff Radu Iosif Space-Reduction Strategies for Model Checking Dynamic Software. 2003 conf/cav/2003smc SoftMC@CAV https://doi.org/10.1016/S1571-0661(05)80009-X db/conf/cav/smc2003.html#RobbyDHI03 499-517 Hubert Garavel John Hatcliff Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings TACAS Lecture Notes in Computer Science 2619 Springer 2003 3-540-00898-5 https://doi.org/10.1007/3-540-36577-X db/conf/tacas/tacas2003.html

James C. Corbett Matthew B. Dwyer John Hatcliff Robby Expressing checkable properties of dynamic systems: the Bandera Specification Language. 34-56 2002 4 Int. J. Softw. Tools Technol. Transf. 1 https://doi.org/10.1007/s100090200075 db/journals/sttt/sttt4.html#CorbettDH02

John Hatcliff Matthew B. Dwyer Corina S. Pasareanu Robby Foundations of the Bandera Abstraction Tools. 172-203 2002 conf/birthday/2002jones The Essence of Computation https://doi.org/10.1007/3-540-36377-7_9 db/conf/birthday/jones2002.html#HatcliffDPR02 Xianghua Deng Matthew B. Dwyer John Hatcliff Georg Jung Robby Gurdip Singh Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. 154-181 https://doi.org/10.1007/978-3-540-39656-7_6 2002 conf/fmco/2002 FMCO db/conf/fmco/fmco2002.html#DengDHJRS02 Xianghua Deng Matthew B. Dwyer John Hatcliff Masaaki Mizuno Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. 442-452 2002 conf/icse/2002 ICSE https://doi.org/10.1145/581339.581394 db/conf/icse/icse2002.html#DengDHM02

Gilles Barthe John Hatcliff Morten Heine Sørensen An induction principle for pure type systems. 773-818 2001 266 Theor. Comput. Sci. 1-2 db/journals/tcs/tcs266.html#BartheHS01 https://doi.org/10.1016/S0304-3975(00)00373-X

Gilles Barthe John Hatcliff Morten Heine Sørensen Weak normalization implies strong normalization in a class of non-dependent pure type systems. 317-361 2001 269 Theor. Comput. Sci. 1-2 db/journals/tcs/tcs269.html#BartheHS01a https://doi.org/10.1016/S0304-3975(01)00012-3

John Hatcliff Matthew B. Dwyer Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. 39-58 2001 conf/concur/2001 CONCUR https://doi.org/10.1007/3-540-44685-0_5 db/conf/concur/concur2001.html#HatcliffD01 Matthew B. Dwyer John Hatcliff Roby Joehanes Shawn Laubach Corina S. Pasareanu Robby Hongjun Zheng Willem Visser Tool-Supported Program Abstraction for Finite-State Verification. 177-187 2001 conf/icse/2001 ICSE db/conf/icse/icse2001.html#DwyerHJLPRZV01 https://doi.org/10.1109/ICSE.2001.919092 https://doi.ieeecomputersociety.org/10.1109/ICSE.2001.919092

John Hatcliff Matthew B. Dwyer Hongjun Zheng Slicing Software for Model Construction. 315-353 2000 13 High. Order Symb. Comput. 4 db/journals/lisp/lisp13.html#HatcliffDZ00 https://doi.org/10.1023/A:1026599015809

Matthew B. Dwyer John Hatcliff Adapting programming languages technologies for finite-state verification. 46-49 2000 25 ACM SIGSOFT Softw. Eng. Notes 1 https://doi.org/10.1145/340855.340885 db/journals/sigsoft/sigsoft25.html#DwyerH00

James C. Corbett Matthew B. Dwyer John Hatcliff Shawn Laubach Corina S. Pasareanu Robby Hongjun Zheng Bandera: extracting finite-state models from Java source code. 439-448 2000 conf/icse/2000 ICSE https://doi.org/10.1145/337180.337234 db/conf/icse/icse2000.html#CorbettDHLPRZ00 James C. Corbett Matthew B. Dwyer John Hatcliff Robby Bandera: a source-level interface for model checking Java programs. 762-765 2000 conf/icse/2000 ICSE https://doi.org/10.1145/337180.337625 db/conf/icse/icse2000.html#CorbettDHR00 James C. Corbett Matthew B. Dwyer John Hatcliff Robby A Language Framework for Expressing Checkable Properties of Dynamic Software. 205-223 2000 conf/spin/2000 SPIN db/conf/spin/spin2000.html#CorbettDHR00 https://doi.org/10.1007/10722468_13

Gilles Barthe John Hatcliff Morten Heine Sørensen CPS Translations and Applications: The Cube and Beyond. 125-170 1999 12 High. Order Symb. Comput. 2 db/journals/lisp/lisp12.html#BartheHS99 https://doi.org/10.1023/A:1010000206149

Matthew B. Dwyer John Hatcliff Slicing Software for Model Construction. 105-118 1999 conf/pepm/1999 PEPM db/conf/pepm/pepm1999.html#DwyerH99 John Hatcliff James C. Corbett Matthew B. Dwyer Stefan Sokolowski Hongjun Zheng A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives. 1-18 1999 conf/sas/1999 SAS https://doi.org/10.1007/3-540-48294-6_1 db/conf/sas/sas99.html#HatcliffCDSZ99 John Hatcliff Torben Æ. Mogensen Peter Thiemann 0001 Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998 Partial Evaluation Lecture Notes in Computer Science 1706 Springer 1999 3-540-66710-5 https://doi.org/10.1007/3-540-47018-2 https://www.wikidata.org/entity/Q117569184 db/conf/pepm/pe1998.html

John Hatcliff Foundations for Partial Evaluation of Functional Programs with Computational Effects. 13 1998 30 ACM Comput. Surv. 3es https://doi.org/10.1145/289121.289134 db/journals/csur/csur30.html#Hatcliff98

Matthew B. Dwyer John Hatcliff Muhammad Nanda Using Partial Evaluation to Enable Verification of Concurrent Software. 22 1998 30 ACM Comput. Surv. 3es https://doi.org/10.1145/289121.289143 db/journals/csur/csur30.html#DwyerHN98

Robert Glück John Hatcliff Jesper Jørgensen Generalization in Hierarchies of Online Program Specialization Systems. 179-198 https://doi.org/10.1007/3-540-48958-4_10 1998 conf/lopstr/1998 LOPSTR db/conf/lopstr/lopstr98.html#GluckHJ98 John Hatcliff An Introduction to Online and Offline Partial Evaluation using a Simple Flowchart Language. 20-82 1998 conf/pepm/1998 Partial Evaluation db/conf/pepm/pe1998.html#Hatcliff98 https://doi.org/10.1007/3-540-47018-2_2 John Hatcliff Matthew B. Dwyer Shawn Laubach Staging Static Analyses Using Abstraction-Based Program Specialization. 134-151 https://doi.org/10.1007/BFb0056612 1998 conf/plilp/1998 PLILP/ALP db/conf/plilp/plilp98.html#HatcliffDL98

John Hatcliff Olivier Danvy Thunks and the lambda-Calculus. 303-319 1997 7 J. Funct. Program. 3 db/journals/jfp/jfp7.html#HatcliffD97 https://doi.org/10.1017/s0956796897002748

John Hatcliff Olivier Danvy A Computational Formalization for Partial Evaluation. 507-541 1997 7 Math. Struct. Comput. Sci. 5 db/journals/mscs/mscs7.html#HatcliffD97 https://doi.org/10.1017/S0960129597002405

Gilles Barthe John Hatcliff Morten Heine Sørensen Reflections on Reflections. 241-258 1997 conf/plilp/1997 PLILP db/conf/plilp/plilp97.html#BartheHS97 https://doi.org/10.1007/BFb0033848 Gilles Barthe John Hatcliff Morten Heine Sørensen A notion of classical pure type system. 1997 conf/mfps/1997 4-59 MFPS https://doi.org/10.1016/S1571-0661(05)80170-7 db/journals/entcs/entcs6.html#BartheHS97 Gilles Barthe John Hatcliff Peter Thiemann 0001 Monadic Type Systems: Pure Type Systems for Impure Settings. 1997 conf/hoots/1997 HOOTS https://doi.org/10.1016/S1571-0661(05)80691-7 db/journals/entcs/entcs10.html#BartheHT97 54-120 John Hatcliff Robert Glück Reasoning about Hierarchies of Online Program Specialization Systems. 161-182 1996 conf/dagstuhl/1996pe Dagstuhl Seminar on Partial Evaluation db/conf/dagstuhl/dagstuhl-pe96.html#HatcliffG96 https://doi.org/10.1007/3-540-61580-6_9 https://www.wikidata.org/entity/Q62038292 John Hatcliff Mechanically Verifying the Correctness of an Offline Partial Evaluator 279-298 conf/plilp/95 PLILP 1995 db/conf/plilp/plilp95.html#Hatcliff95 https://doi.org/10.1007/BFb0026826 John Hatcliff Olivier Danvy A Generic Account of Continuation-Passing Styles. 458-471 1994 conf/popl/1994 POPL db/conf/popl/popl94.html#HatcliffD94 https://doi.org/10.1145/174675.178053 Olivier Danvy John Hatcliff On the Transformation between Direct and Continuation Semantics. 627-648 1993 conf/mfps/1993 MFPS db/conf/mfps/mfps1993.html#DanvyH93 https://doi.org/10.1007/3-540-58027-1_31

Olivier Danvy John Hatcliff CPS-Transformation After Strictness Analysis. 195-212 1992 1 LOPLAS 3 db/journals/loplas/loplas1.html#DanvyH92 https://doi.org/10.1145/151640.151641

Olivier Danvy John Hatcliff Thunks (Continued). 3-11 1992 conf/sas/1992 WSA db/conf/sas/wsa92.html#DanvyH92 Erika Ábrahám Perry Alexander Siddharth Amaravadi Torben Amtoft Isaac Amundson Daniel Andresen Maria-Virginia Aponte Andrew W. Appel David Arney Junaid Babar Mark W. Bailey Anindya Banerjee 0001 Stephen C. Barrett Gilles Barthe Jason Belt Lennart Beringer Ruth Breu Jim Carciofini Todd Carpenter Patrice Chalin Sanjian Chen Adam Childs Rance Cleaveland Darren D. Cofer Cyrille Comar James C. Corbett Pierre Courtieu Andrew Cousino Tristan Crolard Olivier Danvy Julien Delange William Deng Xianghua Deng Josiah Dodds Kyung-Goo Doh Matthew B. Dwyer Lu Feng 0001 Anura Fernando Cormac Flanagan Kim R. Fowler Hubert Garavel Fatemeh Ghassemi Robert Glück Aniruddha S. GokhaleAniruddha Gokhale Julian M. Goldman Jesse Greenwald David A. Greve Jérôme Guitton Richard Habeeb Stefan Hallerstede David S. Hardin Mats P. E. HeimdahlMats Per Erik Heimdahl Jonathan Hoag Karl Hoech Matthew Hoosier Jérôme Hugues Michaela Huhn Radu Iosif Ganeshan Jayaraman Eunkyoung Jee Trevor Jennings Raoul Praful Jetley Roby Joehanes Paul L. Jones Joseph Jorgens Jesper Jørgensen Georg Jung Tim Kelly Ehsan Khamespanah BaekGyu Kim Yu Jin Kim Andrew L. King Gerwin Klein Arvind S. Krishna Bruce H. Krogh Ihor Kuz Brian R. Larson Shawn Laubach Mark Lawford Gary T. Leavens Insup Lee 0001 Peter Lee 0001 Jacob Legg K. Rustan M. Leino Corey Lewis Kejia Li Catalina Liang Alasdair Macdonald T. S. E. Maibaum Clint McKenzie Kent McLeod Eric Mercer Masaaki Mizuno Torben Æ. Mogensen Yannick Moy Margaret Mullen-Fortino Peter Müller 0001 Muhammad Nanda Mitchell L. Neilsen Xinming Ou George J. Pappas Soojin Park Matthew J. Parkinson Corina PasareanuCorina S. Pasareanu Sam Procter S. Raj Rajagopalan Venkatesh Prasad RanganathVenkatesh-Prasad Ranganath Robby Michael Robkin Edwin Rodríguez Alex Roederer Harvey Rubin Douglas C. Schmidt Lui Sha John Shackleton Prashant Shanti Gurdip Singh Marjan Sirjani Konrad Slind Stefan Sokolowski Oleg Sokolsky Morten Heine Sørensen William Spees Danielle Stewart Hariharan Thiagarajan Peter Thiemann 0001 Frank Tip Gabriele Trombetti Srivatsan Varadarajan Eugene Y. Vasserman Krishna K. Venkatasubramanian Willem Visser Noah Abou El Wafa Todd Wallentine Xiaolong Wang Steve Warren Alan Wassyng Jens H. Weber Sandy Weininger Lutz Wrage Fred L. Wurden Mahsa Zarneshan Yi Zhang 0051 Zhi Zhang Hongjun Zheng Elena Zucca