John Hatcliff - RankMe

147 papers A* 9A 7B 15C 16Misc 2Journal 40Unranked 52

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A mechanized semantics for component-based systems in the HAMR AADL runtime. Sci. Comput. Program. Stefan Hallerstede, John Hatcliff
2025	J	`jnl`	Automated property-based testing from AADL component contracts. Int. J. Softw. Tools Technol. Transf. John Hatcliff, Jason Belt, Robby, Jacob Legg, Danielle Stewart, Todd Carpenter
2025	C	`conf`	End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR. FMICS John Hatcliff, Jason Belt, Robby, Clint McKenzie, Catalina Liang
2025	J	`jnl`	Logika: the Sireum verification framework. Int. J. Softw. Tools Technol. Transf. Robby, John Hatcliff, Jason Belt
2025	C	`conf`	Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. FMICS Stefan Hallerstede, Robby, John Hatcliff, Jason Belt, David S. Hardin
2025	—	`conf`	The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering. The Combined Power of Research, Education, and Dissemination John Hatcliff, Jason Belt
2024	—	`conf`	Integrated Contract-Based Unit and System Testing for Component-Based Systems. NFM John Hatcliff, Jason Belt, Robby, David S. Hardin
2024	C	`conf`	Logika: The Sireum Verification Framework. FMICS Robby, John Hatcliff, Jason Belt
2024	—	`conf`	Teaching with Logika: Conceiving and Constructing Correct Software. FMTea Stefan Hallerstede, John Hatcliff, Robby
2023	—	`conf`	A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime. FACS Stefan Hallerstede, John Hatcliff
2023	C	`conf`	Automated Property-Based Testing from AADL Component Contracts. FMICS John Hatcliff, Jason Belt, Robby, Jacob Legg, Danielle Stewart, Todd Carpenter
2023	J	`jnl`	Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041). Dagstuhl Reports Erika Ábrahám, Stefan Hallerstede, John Hatcliff, Danielle Stewart, Noah Abou El Wafa
2023	J	`jnl`	Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. 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
2022	J	`jnl`	Awas: AADL information flow and error propagation analysis framework. Innov. Syst. Softw. Eng. Hariharan Thiagarajan, John Hatcliff, Robby
2022	J	`jnl`	Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 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
2022	—	`conf`	Formalization of the AADL Run-Time Services. ISoLA (2) John Hatcliff, Jérôme Hugues, Danielle Stewart, Lutz Wrage
2022	C	`conf`	Mechanization of a Large DSML: An Experiment with AADL and Coq. MEMOCODE Jérôme Hugues, Lutz Wrage, John Hatcliff, Danielle Stewart
2022	J	`jnl`	Specification and Verification of Timing Properties in Interoperable Medical Systems. Log. Methods Comput. Sci. Mahsa Zarneshan, Fatemeh Ghassemi, Ehsan Khamespanah, Marjan Sirjani, John Hatcliff
2021	C	`conf`	HAMR: An AADL Multi-platform Code Generation Toolset. ISoLA John Hatcliff, Jason Belt, Robby, Todd Carpenter
2021	C	`conf`	Slang: The Sireum Programming Language. ISoLA Robby, John Hatcliff
2020	—	`conf`	Awas: AADL Information Flow and Error Propagation Analysis Framework. ECSA Companion Hariharan Thiagarajan, John Hatcliff, Robby
2020	—	`conf`	Model-Based Risk Analysis for an Open-Source PCA Pump Using AADL Error Modeling. IMBSA Hariharan Thiagarajan, Brian R. Larson, John Hatcliff, Yi Zhang
2020	J	`jnl`	Specification and Verification of Timing Properties in Interoperable Medical Systems. CoRR Mahsa Zarneshan, Fatemeh Ghassemi, Ehsan Khamespanah, Marjan Sirjani, John Hatcliff
2019	J	`jnl`	The open PCA pump project: an exemplar open source medical device as a community resource. SIGBED Rev. John Hatcliff, Brian R. Larson, Todd Carpenter, Paul L. Jones, Yi Zhang, Joseph Jorgens
2018	—	`conf`	A Unified Approach for Modeling, Developing, and Assuring Critical Systems. ISoLA (1) John Hatcliff, Brian R. Larson, Jason Belt, Robby, Yi Zhang
2018	—	`conf`	Assurance Case Considerations for Interoperable Medical Systems. SAFECOMP Workshops Yi Zhang, Brian R. Larson, John Hatcliff
2018	—	`conf`	Model-Based Development for High-Assurance Embedded Systems. ISoLA (1) Robby, John Hatcliff, Jason Belt
2017	—	`conf`	A Reference Separation Architecture for Mixed-Criticality Medical and IoT Devices. SafeThings@SenSys Todd Carpenter, John Hatcliff, Eugene Y. Vasserman
2017	—	`conf`	Enhanced Security of Building Automation Systems Through Microkernel-Based Controller Platforms. ICDCS Workshops Xiaolong Wang, Richard Habeeb, Xinming Ou, Siddharth Amaravadi, John Hatcliff, Masaaki Mizuno, Mitchell L. Neilsen, S. Raj Rajagopalan, Srivatsan Varadarajan
2017	B	`conf`	Focused Certification of an Industrial Compilation and Static Verification Toolchain. SEFM Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu
2017	B	`conf`	SAFE and Secure: Deeply Integrating Security in a New Hazard Analysis. ARES Sam Procter, Eugene Y. Vasserman, John Hatcliff
2015	—	`conf`	Communication patterns for interconnecting and composing medical systems. EMBC Venkatesh-Prasad Ranganath, Yu Jin Kim, John Hatcliff, Robby
2015	—	`conf`	Ecosphere Principles for Medical Application Platforms. ICHI Yu Jin Kim, Sam Procter, John Hatcliff, Venkatesh-Prasad Ranganath, Robby
2015	J	`jnl`	Enabling Safe Interoperation by Medical Device Virtual Integration. IEEE Des. Test Brian R. Larson, Yi Zhang, Stephen C. Barrett, John Hatcliff, Paul L. Jones
2015	—	`conf`	Error Type Refinement for Assurance of Families of Platform-Based Systems. SAFECOMP Workshops Sam Procter, John Hatcliff, Sandy Weininger, Anura Fernando
2015	B	`conf`	Towards Assurance for Plug & Play Medical Systems. SAFECOMP Andrew L. King, Lu Feng, Sam Procter, Sanjian Chen, Oleg Sokolsky, John Hatcliff, Insup Lee
2014	C	`conf`	An architecturally-integrated, systems-based hazard analysis for medical applications. MEMOCODE Sam Procter, John Hatcliff
2014	—	`conf`	Certifiably safe software-dependent systems: challenges and directions. FOSE John Hatcliff, Alan Wassyng, Tim Kelly, Cyrille Comar, Paul L. Jones
2014	—	`conf`	Towards an AADL-Based Definition of App Architecture for Medical Application Platforms. FHIES/SEHC Sam Procter, John Hatcliff, Robby
2013	—	`conf`	BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. NASA Formal Methods Brian R. Larson, Patrice Chalin, John Hatcliff
2013	A*	`conf`	Explicating symbolic execution (xSymExe): an evidence-based verification framework. ICSE John Hatcliff, Robby, Patrice Chalin, Jason Belt
2013	Misc	`conf`	Foundational Security Principles for Medical Application Platforms - (Extended Abstract). WISA Eugene Y. Vasserman, John Hatcliff
2013	—	`conf`	Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device. HILT Brian R. Larson, John Hatcliff, Kim R. Fowler, Julien Delange
2013	—	`conf`	Open source patient-controlled analgesic pump requirements documentation. SEHC@ICSE Brian R. Larson, John Hatcliff, Patrice Chalin
2013	—	`ed.`	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 Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh, John Hatcliff
2013	J	`jnl`	Software Certification: Methods and Tools (Dagstuhl Seminar 13051). Dagstuhl Reports Darren D. Cofer, John Hatcliff, Michaela Huhn, Mark Lawford
2013	—	`conf`	Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. HILT Pierre Courtieu, Maria-Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings
2012	—	`conf`	A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. POST Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino
2012	C	`conf`	Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. SCAM Hariharan Thiagarajan, John Hatcliff, Jason Belt, Robby
2012	J	`jnl`	Behavioral interface specification languages. ACM Comput. Surv. John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
2012	J	`jnl`	Challenges and Research Directions in Medical Cyber-Physical Systems. Proc. IEEE 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
2012	—	`conf`	Component-based app design for platform-oriented devices in a medical device coordination framework. IHI Kejia Li, Steve Warren, John Hatcliff
2012	—	`conf`	Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. NASA Formal Methods Jason Belt, Robby, Patrice Chalin, John Hatcliff, Xianghua Deng
2012	—	`conf`	Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. HILT Jason Belt, Patrice Chalin, John Hatcliff, Robby
2012	—	`ed.`	Proceedings of the 4th International Workshop on Software Engineering in Health Care, SEHC 2012, Zurich, Switzerland, June 4-5, 2012 SEHC@ICSE Ruth Breu, John Hatcliff
2012	—	`conf`	Rationale and Architecture Principles for Medical Application Platforms. ICCPS John Hatcliff, Andrew L. King, Insup Lee, Alasdair Macdonald, Anura Fernando, Michael Robkin, Eugene Y. Vasserman, Sandy Weininger, Julian M. Goldman
2012	—	`conf`	Requirements specification for apps in medical application platforms. SEHC@ICSE Brian R. Larson, John Hatcliff, Sam Procter, Patrice Chalin
2011	—	`conf`	Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. NASA Formal Methods Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
2011	—	`conf`	Enhancing spark's contract checking facilities using symbolic execution. SIGAda Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
2010	J	`jnl`	A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. Sci. Comput. Program. Georg Jung, John Hatcliff
2010	—	`ed.`	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 FMOODS/FORTE John Hatcliff, Elena Zucca
2010	A	`conf`	Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. ESOP Torben Amtoft, John Hatcliff, Edwin Rodríguez
2010	—	`conf`	Prototyping closed loop physiologic control with the medical device coordination framework. SEHC@ICSE Andrew L. King, David Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, Sam Procter
2010	—	`conf`	Software certification consortium: certification methods for safety-critical software. CASCON Alan Wassyng, Mark Lawford, T. S. E. Maibaum, Jens H. Weber, John Hatcliff
2010	—	`ch.`	Specification and Checking of Software Contracts for Conditional Information Flow. Design and Verification of Microprocessor Systems for High-Assurance Applications Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve
2009	J	`jnl`	A publish-subscribe architecture and component-based programming model for medical device interoperability. SIGBED Rev. Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
2009	—	`conf`	An open test bed for medical device integration and coordination. ICSE Companion Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
2009	—	`conf`	Demonstration of a medical device integration and coordination framework. ICSE Companion Andrew L. King, Sam Procter, Daniel Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Praful Jetley, Paul L. Jones, Sandy Weininger
2008	—	`conf`	A Software Certification Consortium and its Top 9 Hurdles. SafeCert@ETAPS John Hatcliff, Mats Per Erik Heimdahl, Mark Lawford, T. S. E. Maibaum, Alan Wassyng, Fred L. Wurden
2008	C	`conf`	Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows. ICFEM John Hatcliff
2008	B	`conf`	Specification and Checking of Software Contracts for Conditional Information Flow. FM Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve
2007	J	`jnl`	A correlation framework for the CORBA component model. Int. J. Softw. Tools Technol. Transf. Georg Jung, John Hatcliff
2007	J	`jnl`	A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, John Hatcliff, Matthew B. Dwyer
2007	B	`conf`	A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. GPCE Georg Jung, John Hatcliff
2007	—	`conf`	Formal Software Analysis Emerging Trends in Software Model Checking. FOSE Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser
2007	J	`jnl`	Slicing concurrent Java programs using Indus and Kaveri. Int. J. Softw. Tools Technol. Transf. Venkatesh Prasad Ranganath, John Hatcliff
2007	B	`conf`	Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. SEFM Xianghua Deng, Robby, John Hatcliff
2006	—	`conf`	Bogor: A Flexible Framework for Creating Software Model Checkers. TAIC PART Robby, Matthew B. Dwyer, John Hatcliff
2006	J	`jnl`	CALM and Cadena: Metamodeling for Component-Based Product-Line Development. Computer Adam Childs, Jesse Greenwald, Georg Jung, Matthew Hoosier, John Hatcliff
2006	J	`jnl`	Checking JML specifications using an extensible software model checking framework. Int. J. Softw. Tools Technol. Transf. Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
2006	A*	`conf`	Domain-specific Model Checking Using The Bogor Framework. ASE Robby, Matthew B. Dwyer, John Hatcliff
2006	A	`conf`	Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. TACAS Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine
2006	J	`jnl`	High-Confidence Medical Device Software and Systems. Computer Insup Lee, George J. Pappas, Rance Cleaveland, John Hatcliff, Bruce H. Krogh, Peter Lee, Harvey Rubin, Lui Sha
2006	J	`jnl`	Introduction to special issue. SIGBED Rev. John Hatcliff, Insup Lee, Oleg Sokolsky
2006	C	`conf`	Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. ISoLA Xianghua Deng, Robby, John Hatcliff
2006	J	`jnl`	PEPM 2006 paper abstracts. ACM SIGPLAN Notices Mark W. Bailey, John Hatcliff, Frank Tip
2006	C	`ed.`	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 John Hatcliff, Frank Tip
2006	J	`jnl`	TACAS 2003 Special Issue - Preface. Theor. Comput. Sci. Hubert Garavel, John Hatcliff
2006	J	`jnl`	Towards highly optimized real-time middleware for software product-line architectures. SIGBED Rev. Arvind S. Krishna, Aniruddha S. Gokhale, Douglas C. Schmidt, Venkatesh Prasad Ranganath, John Hatcliff
2006	J	`jnl`	Why you should definitely read this special section. Int. J. Softw. Tools Technol. Transf. Hubert Garavel, John Hatcliff
2005	A	`conf`	A New Foundation for Control-Dependence and Slicing for Modern Program Structures. ESOP Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff
2005	—	`ch.`	An Integrated Model-Driven Development Environment for Composing and Validating Distributed Real-Time and Embedded Systems. Model-Driven Software Development Gabriele Trombetti, Aniruddha Gokhale, Douglas C. Schmidt, Jesse Greenwald, John Hatcliff, Georg Jung, Gurdip Singh
2005	A*	`conf`	Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. CAV Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby
2005	A	`conf`	Extending JML for Modular Specification and Verification of Multi-threaded Programs. ECOOP Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby
2005	B	`conf`	Kaveri: Delivering the Indus Java Program Slicer to Eclipse. FASE Ganeshan Jayaraman, Venkatesh Prasad Ranganath, John Hatcliff
2005	J	`jnl`	Translating Java for Multiple Model Checkers: The Bandera Back-End. Formal Methods Syst. Des. Radu Iosif, Matthew B. Dwyer, John Hatcliff
2004	C	`conf`	A Case Study in Domain-Customized Model Checking for Real-Time Component Software. ISoLA Matthew Hoosier, Matthew B. Dwyer, Robby, John Hatcliff
2004	—	`conf`	A Case Study in Domain-customized Model Checking for Real-time Component Software. ISoLA (Preliminary proceedings) Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer
2004	B	`conf`	A Correlation Framework for the CORBA Component Model. FASE Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath
2004	—	`conf`	A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. CASSIS Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff, Robby
2004	B	`conf`	Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems. FASE Adam Childs, Jesse Greenwald, Venkatesh Prasad Ranganath, Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Prashant Shanti, Gurdip Singh
2004	A	`conf`	Checking Strong Specifications Using an Extensible Software Model Checking Framework. TACAS Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
2004	J	`jnl`	Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs. Formal Methods Syst. Des. Matthew B. Dwyer, John Hatcliff, Robby, Venkatesh Prasad Ranganath
2004	B	`conf`	Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. CC Venkatesh Prasad Ranganath, John Hatcliff
2004	—	`conf`	Supporting model checking education using BOGOR/Eclipse. eTX Matthew B. Dwyer, John Hatcliff, Matthew Hoosier
2004	A	`conf`	SyncGen: An Aspect-Oriented Framework for Synchronization. TACAS Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno
2004	B	`conf`	Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. VMCAI John Hatcliff, Robby, Matthew B. Dwyer
2003	—	`conf`	Bogor: an extensible and highly-modular software model checking framework. ESEC / SIGSOFT FSE Robby, Matthew B. Dwyer, John Hatcliff
2003	A*	`conf`	Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems. ICSE John Hatcliff, Xianghua Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath
2003	—	`conf`	Cadena: enabling CCM-based application development in Eclipse. eTX Venkatesh Prasad Ranganath, Adam Childs, Jesse Greenwald, Matthew B. Dwyer, John Hatcliff, Gurdip Singh
2003	C	`conf`	Slicing and partial evaluation of CORBA component model designs for avionics system. PEPM John Hatcliff, William Deng, Matthew B. Dwyer, Georg Jung, Venkatesh Prasad Ranganath, Robby
2003	Misc	`conf`	Space Reductions for Model Checking Quasi-Cyclic Systems. EMSOFT Matthew B. Dwyer, Robby, Xianghua Deng, John Hatcliff
2003	—	`conf`	Space-Reduction Strategies for Model Checking Dynamic Software. SoftMC@CAV Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif
2003	A	`ed.`	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 Hubert Garavel, John Hatcliff
2002	J	`jnl`	Expressing checkable properties of dynamic systems: the Bandera Specification Language. Int. J. Softw. Tools Technol. Transf. James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
2002	—	`conf`	Foundations of the Bandera Abstraction Tools. The Essence of Computation John Hatcliff, Matthew B. Dwyer, Corina S. Pasareanu, Robby
2002	A*	`conf`	Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. ICSE Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno
2002	—	`conf`	Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. FMCO Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh
2001	J	`jnl`	An induction principle for pure type systems. Theor. Comput. Sci. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
2001	A*	`conf`	Tool-Supported Program Abstraction for Finite-State Verification. ICSE Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng, Willem Visser
2001	B	`conf`	Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. CONCUR John Hatcliff, Matthew B. Dwyer
2001	J	`jnl`	Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theor. Comput. Sci. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
2000	—	`conf`	A Language Framework for Expressing Checkable Properties of Dynamic Software. SPIN James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
2000	J	`jnl`	Adapting programming languages technologies for finite-state verification. ACM SIGSOFT Softw. Eng. Notes Matthew B. Dwyer, John Hatcliff
2000	A*	`conf`	Bandera: a source-level interface for model checking Java programs. ICSE James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
2000	A*	`conf`	Bandera: extracting finite-state models from Java source code. ICSE James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng
2000	J	`jnl`	Slicing Software for Model Construction. High. Order Symb. Comput. John Hatcliff, Matthew B. Dwyer, Hongjun Zheng
1999	B	`conf`	A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives. SAS John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, Hongjun Zheng
1999	J	`jnl`	CPS Translations and Applications: The Cube and Beyond. High. Order Symb. Comput. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1999	—	`ed.`	Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998 Partial Evaluation John Hatcliff, Torben Æ. Mogensen, Peter Thiemann
1999	C	`conf`	Slicing Software for Model Construction. PEPM Matthew B. Dwyer, John Hatcliff
1998	—	`conf`	An Introduction to Online and Offline Partial Evaluation using a Simple Flowchart Language. Partial Evaluation John Hatcliff
1998	J	`jnl`	Foundations for Partial Evaluation of Functional Programs with Computational Effects. ACM Comput. Surv. John Hatcliff
1998	C	`conf`	Generalization in Hierarchies of Online Program Specialization Systems. LOPSTR Robert Glück, John Hatcliff, Jesper Jørgensen
1998	—	`conf`	Staging Static Analyses Using Abstraction-Based Program Specialization. PLILP/ALP John Hatcliff, Matthew B. Dwyer, Shawn Laubach
1998	J	`jnl`	Using Partial Evaluation to Enable Verification of Concurrent Software. ACM Comput. Surv. Matthew B. Dwyer, John Hatcliff, Muhammad Nanda
1997	J	`jnl`	A Computational Formalization for Partial Evaluation. Math. Struct. Comput. Sci. John Hatcliff, Olivier Danvy
1997	B	`conf`	A notion of classical pure type system. MFPS Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1997	—	`conf`	Monadic Type Systems: Pure Type Systems for Impure Settings. HOOTS Gilles Barthe, John Hatcliff, Peter Thiemann
1997	—	`conf`	Reflections on Reflections. PLILP Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1997	J	`jnl`	Thunks and the lambda-Calculus. J. Funct. Program. John Hatcliff, Olivier Danvy
1996	—	`conf`	Reasoning about Hierarchies of Online Program Specialization Systems. Dagstuhl Seminar on Partial Evaluation John Hatcliff, Robert Glück
1995	—	`conf`	Mechanically Verifying the Correctness of an Offline Partial Evaluator PLILP John Hatcliff
1994	A*	`conf`	A Generic Account of Continuation-Passing Styles. POPL John Hatcliff, Olivier Danvy
1993	B	`conf`	On the Transformation between Direct and Continuation Semantics. MFPS Olivier Danvy, John Hatcliff
1992	J	`jnl`	CPS-Transformation After Strictness Analysis. LOPLAS Olivier Danvy, John Hatcliff
1992	—	`conf`	Thunks (Continued). WSA Olivier Danvy, John Hatcliff