Papers

Below are some of my publications.

I am working on reorganizing my publications and associated links. Some of the links are currently not working. My new organization makes use of DOIs. To find out how DOIs are used, go here.


Edited Journal Issues

  • Garavel, Hubert(ed.) and Hatcliff, John(ed). Special Issue of International Journal for Software Tools for Technology Transfer (STTT) (Springer) (Volume 8, Number 1 / February, 2006) dedicated to selected papers from Ninth Annual Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003). (pdf [updated: August 9, 2004], bibtxt) (Garavel-Hatcliff:TACAS03-STTT06)
  • Garavel, Hubert(ed.) and Hatcliff, John (ed). Special Issue of Theoretical Computer Science (Volume 354, Issue 2) dedicated to selected papers from Ninth Annual Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003). (bibtxt)
  • (Garavel-Hatcliff:TACAS03-TCS06)

Edited Volumes/Proceedings

  • Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (SAIRP 2013). EPTCS 129, 2013. Anindya Banerjee, Olivier Danvy, Kyung-goo Doh, John Hatcliff (editors).
  • Proceedings of the Fourth Workshop on Software Engineering in Health Care, June 2012, A workshop affiliated with the 2012 International Conference on Software Engineering, Zurich, Switzerland. Ruth Breu and John Hatcliff (editors).
  • Formal Techniques for Distributed Systems, Proceedings of the Joint 12th IFIP WG6.1 International Conference, FMOODS 2010 and 30th IFIP WG6.1 International Conference, FORTE 2010, Amsterdam, The Netherlands, June 2010. John Hatcliff and Elena Zucca (editors) Lecture Notes in Computer Science (LNCS) 2619, Springer, 2010.
  • Garavel, Hubert(ed.) and John Hatcliff(ed). Proceedings of the Ninth Annual Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003). Lecture Notes in Computer Science (LNCS) 2619, Springer-Verlag, 2003. (bibtxt) (Garavel-Hatcliff:TACAS03)
  • Hatcliff, John, Torben Mogensen and Peter Thiemann(editors). Proceedings of the DIKU 1998 International Summerschool on Partial Evaluation. Lecture Notes in Computer Science (LNCS) 1706, Springer-Verlag, 1998. (acm portal, bibtxt) (Hatcliff-al:DIKU-ISPE98)

Invited papers and book chapters

  • "Certifiably Safe Software-Dependent Systems: Challenges and Directions", John Hatcliff, Alan Wassyng, Tim Kelly, Cyrille Comar, and Paul Jones. Future of Software Engineering, 2014 International Conference on Software Engineering (ICSE 2014). (DOI, acm portal)
  • "Specification and Checking of Software Contracts for Conditional Information Flow (extended version)", Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag, and David Greve. Invited book chapter in Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 341--380. Springer, 2010. ISBN 978-1-4419-1538-2.
  • Hatcliff, John, Matthew B. Dwyer, Corina S.Puasuareanu, and Robby; Torben Mogensen(ed.), Hal Sudborough(ed.), and Dave Schmidt(ed.). "Foundations of the Bandera Abstraction Tools." pp. 172 – 203. In "The Essence of Computation – Essays dedicted to Neil Jones". Lecture Notes in Computer Science 2566. (acm portal, bibtxt) (Hatcliff-al:Jones02)
  • Hatcliff, John. "Partial Evaluation." Olivier Danvy. Encyclopedia of Computer Science. Nature Publishing Group, UK, 2000. (.ps.gz, bibtxt) (Hatcliff-Danvy:EoCS00)
  • "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, In Model-Driven Software Development, Beydeda, Sami; Book, Matthias; Gruhn, Volker (Eds.) 2005, ISBN: 3-540-25613-X, pp. 329–362. (Trombetti-al:MDSD05)

Journal Publications

  • John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson. "Behavioral interface specification languages." ACM Comput. Surveys. 44(3): 16 (2012).
  • Insup Lee, Oleg Sokolsky, S. Chen, John Hatcliff, E. Jee, B. Kim, Andrew King, M. Fortino-Mullen, S. Park, A. Roederer, and K. K. Venkatasubramanian, "Challenges and Research Directions in Medical Cyber-Physical Systems", In Proceedings of the IEEE, 100 (1), pp. 75 - 90, January 2012.
  • Georg Jung and John Hatcliff. "A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures." Science of Computer Programming, 75 (1) July 2010, pp. 615-637 (DOI)
  • Amtoft, Torben, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff, and Venkatesh Prasad Ranganath. "A New Foundation For Control-Dependence and Slicing for Modern Program Structures." ACM Transactions of Programming Languages and Systems. Volume 29, Issue 5, August 2007. (.pdf) (Amtoft-al:TOPLAS07)
  • Jung,Georg and John Hatcliff. "An Event Correlation Framework for the CORBA Component Model." Journal of Software Tools for Technology Transfer. 9 (5) October 2007, pp. 417-427. (Jung-Hatcliff:STTT07) (DOI)
  • "Slicing Concurrent Java Programs using Indus and Kaveri", Journal of Software Tools for Technology Transfer, 9 (5) October 2007, pp. 489-504. (Ranganath-Hatcliff:STTT07) (DOI)
  • Insup Lee, George J. Pappas, Rance Cleaveland, John Hatcliff, Bruce H. Krogh, Peter Lee, Harvey Rubin, Lui Sha, "High-Confidence Medical Device Software and Systems," Computer, vol. 39, no. 4, pp. 33-38, Apr., 2006. (Lee-al:IEEE-Computer06) (DOI, acm portal, bibtxt)
  • Childs, Adam, Jesse Greenwald, Georg Jung, Matthew Hoosier, and John Hatcliff. "CALM and Cadena: Meta-modeling for Component-Based Product-Line Development." IEEE Computer. Vol. 39, No. 2. February, 2006. pp. 42-50. (Childs-al:IEEE-Computer06) (DOI, acm portal, bibtxt)
  • Matthew Dwyer, John Hatcliff, Venkatesh Ranganath, and Robby. "Exploiting Object Escape and Locking Information in Partial Order Reductions for Concurrent Object-Oriented Programs." Journal of Formal Methods in System Design. 25(2). Sep 2004. pp. 199-240. (Dwyer-al:FMSD04) (pdf, DOI, bibtxt)
  • Dwyer, Matthew, John Hatcliff, and Radu Iosif. "Translating Java for Multiple Model Checkers: the Bandera Back-End." Journal of Formal Methods in System Design (Kluwer). Volume 26, Issue 2. March 2005. pp. 137–180. (Dwyer-al:FMSD05) (pdf, DOI, acm portal, bibtxt)
  • "Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language", James Corbett, Matthew Dwyer, John Hatcliff, Robby. Journal of Software Tools for Technology Transfer, 4(1):34-56, 2002. Springer-Verlag. (Corbett-al:STTT02) (abstract, pdf, .ps.gz)
  • Gilles Barthe, John Hatcliff, Morten Heine Soerensen, "Weak Normalization Implies Strong Normalization in Generalized Non-dependent Pure Type Systems", Journal of Theoretical Computer Science, 269(1-2): 317–361, 2001. (Barthe-al:Norm-TCS01) (bibtxt)
  • Gilles Barthe, John Hatcliff, Morten Heine Soerensen, "An Induction Principle for Pure Type Systems", Journal of Theoretical Computer Science, 266(1-2): 773-818, 2001. (Barthe-al:Ind-TCS01) (abstract, .ps.gz, DOI, acm portal, bibtxt)
  • John Hatcliff, Matthew B. Dwyer, Hongjun Zheng, "Slicing Software for Model Construction", Journal of Higher-order and Symbolic Computation, 13(4), pp. 315–353, December, 2000. A special issue containing selected papers from the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. (Hatcliff-al:HOSC00) (abstract, .ps.gz, DOI, acm portal, bibtxt)
  • John Hatcliff, "Foundations for Partial Evaluation of Functional Languages with Computational Effects", 1998 Symposium on Partial Evaluation, ACM Computing Surveys 30(3es), Sept, 1998. (Hatcliff:CS98) (abstract, .ps.gz, DOI, acm portal)
  • Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda, "Using Partial Evaluation to Enable Verification of Concurrent Software", 1998 Symposium on Partial Evaluation, ACM Computing Surveys 30(3es), Sept, 1998. (Dwyer-al:CS98) (abstract, .ps.gz, DOI, acm portal)
  • Gilles Barthe, John Hatcliff, Morten Heine Soerensen, "CPS Translations and Applications: the Cube and Beyond", Journal of Higher-order and Symbolic Computation 12(2), pp. 129 – 170, September, 1999. (Barthe-al:HOSC99) (abstract, .ps.gz, DOI, acm portal)
  • John Hatcliff and Olivier Danvy, "A Computational Formalization for Partial Evaluation", Journal of Mathematical Structures in Computer Science, vol 7, 1997, pp. 507 – 541. Special issue dedicated to the workshop on Logic, Domains, and Programming Languages, Darmstadt, Germany, May 1995. (Hatcliff-Danvy:MSCS97) (.ps.gz, extended.ps.gz[extended version with proofs], DOI, acm portal)
  • Olivier Danvy and John Hatcliff, "CPS Transformation after Strictness Analysis," ACM Letters on Programming Languages and Systems, 1(3):195-212, 1993. (Danvy-Hatcliff:LOPLAS93) (.ps.Z, DOI, acm portal)
  • Olivier Danvy and John Hatcliff, "Thunks (continued)," Proceedings of the Workshop on Static Analysis WSA ’92. Bigre Journal, 81-82:3-11, 1992. (Danvy-Hatcliff:WSA92) (.ps.Z, .pdf)
  • "Thunks and the Lambda-calculus," John Hatcliff and Olivier Danvy, Journal of Functional Programming, 7(3), 1997, pp. 303 – 319. (Hatcliff-Danvy:JFP97) (DOI, acm portal)

Refereed Publications in Conference Proceedings

  • Sam Procter, John Hatcliff. “An Architecturally-Integrated, Systems-Based Hazard Analysis for Medical Applications.” Proceedings of the International Conference on Formal Methods and Models for System Design (MEMOCODE 2014), October 2014
  • Sam Procter, John Hatcliff, Robby. “Towards an AADL-Based Definition of App Architecture for Medical Application Platforms.” Proceedings of the 2014 Software Engineering in Health-care (SEHC) Workshop at the International Symposium on Foundations of Health Information Engineering and Systems (FHIES 2014), July 2014
  • Eugene Y. Vasserman, John Hatcliff, "Foundational Security Principles for Medical Application Platforms", Information Security Applications 2013, pp. 213-217.
  • Brian Larson, John Hatcliff, Patrice Chalin. "Open Source Patient-Controlled Analgesic Pump Requirements Documentation", Proceedings of the 2013 ICSE Workshop on Software Engineering in Health Care, San Francisco, CA. May, 2013.
  • Brian R. Larson, Patrice Chalin, John Hatcliff: "BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software." Proceedings of the 2013 NASA Formal Methods Conference, pp. 276-290.
  • John Hatcliff, Robby, Patrice Chalin, and Jason Belt. 2013. "Explicating symbolic execution (xSymExe): an evidence-based verification framework." In Proceedings of the 2013 International Conference on Software Engineering (ICSE '13). IEEE Press, Piscataway, NJ, USA, 222-231.
  • Brian Larson, John Hatcliff, Sam Procter, Patrice Chalin. "Requirements specification for apps in medical application platforms", Fourth International Workshop on Software Engineering in Health Care, pp. 26-32, June, 2012.
  • John Hatcliff, Andrew King, Insup Lee, Alisdair Macdonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger, Julian Goldman. "Rationale and Architecture Principles for Medical Application Platforms", Proceedings of the 2012 International Conference on Cyber-Physical Systems, pp. 3-12, April, 2012.
  • Jason Belt, Robby, Patrice Chalin, John Hatcliff and Xianghua Deng. "Efficient Symbolic Execution of Value-based Data Structures for Critical Systems'' . Proceedings of the 4th NASA Formal Methods Symposium, pp. 295-309. April, 2012.
  • Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino. "A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow", Proceedings of the 2012 Conference on Principles of Security and Trust, March 2012.
  • Kejia Li, Steve Warren and John Hatcliff, "Component-Based App Design for Platform-Oriented Devices in a Medical Device Coordination Framework", Proceedings of the 2012 ACM SIGHIT International Health Informatics Symposium (IHI 2012), January 2012.
  • Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, and Xianghua Deng. "Enhancing spark's contract checking facilities using symbolic execution." In Proceedings of the 2011 ACM annual international conference on Special interest group on the Ada programming language (SIGAda '11). ACM, New York, NY, USA, pp. 47-60.
  • Jason Belt and John Hatcliff and Robby and Patrice Chalin and David Hardin and Xianghua Deng. "Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution'' Proceedings of the 3rd NASA Formal Methods Symposium, M. Bobaru et al. (Eds.): NFM 2011, LNCS 6617, pp. 58-72. April, 2011.
  • Andrew King, Dave Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, and Sam Procter. "Prototyping closed loop physiologic control with the medical device coordination framework," Proceedings of the 2010 ICSE Workshop on Software Engineering in Health Care, pp. 1-11 Cape Town, South Africa, 2010. ISBN:978-1-60558-973-2. (DOI, ACM portal)
  • Torben Amtoft, John Hatcliff, and Edwin Rodriguez, "Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays", Proceedings of the 2010 European Symposium on Programming (ESOP 2010), LNCS 6012, pp. 43 - 63, March 2010.
  • Andrew King, Sam Procter, Dan Andresen, John Hatcliff, Steve Warren, William Spees, Raoul Jetley, Paul Jones, Sandy Weininger. "An Open Test Bed for Medical Device Integration and Coordination'', Proceedings of International Conference on Software Engineering (ICSE 2009), (Software Engineering in Practice Track). ICSE-Companion 2009. 31st International Conference on Software Engineering, May 2009, pp. 141 - 151. IEEE Press, May 2009.
  • Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag, and David Greve, "Specification and Checking of Software Contracts for Conditional Information Flow", Proceedings of the 2008 International Conference on Formal Methods (FM '08), LNCS 5014, May 2008.
  • Georg Jung and John Hatcliff. "A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures." Proceedings of the 6th International Conference on Generative Programming and Component Engineering, pp. 33 - 42, October, 2007. ACM Press. (bibtex, abstract, DOI, acm portal)
  • Xianghua (William) Deng, Robby, John Hatcliff. "Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems", Proceedings of the 2007 International Conference on Testing: Academic and Industrial Conference: Practice and Research Techniques, IEEE Press, September 2007. (bibtex, abstract,.pdf of extended version)
  • Xianghua Deng, Robby, and John Hatcliff. "Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs", Proceedings of the 2007 International Conference on Software Engineering and Formal Methods, September 2007. (bibtex, abstract,.pdf of extended version, DOI, acm portal)
  • Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Psreanu, Willem Visser. "Formal Software Analysis : Emerging Trends in Software Model Checking." Future of Software Engineering Track. Proceedings of the 2007 International Conference on Software Engineering (ICSE 2007). May, 2007. (DOI, acm portal)
  • Robby, Matthew Dwyer, and John Hatcliff, "Bogor: A Flexible Framework for Creating Software Model Checkers", Proceedings of the International Conference on Testing: Academic and Industrial Conference: Practice and Research Techniques, IEEE Press, August 2006. (DOI, acm portal)
  • Venkatesh Ranganath, John Hatcliff, "An Overview of the Indus Framework for Analysis and Slicing of Concurrent Java Software", Proceedings of the 2006 IEEE Workshop on Source Code Analysis and Manipulation (SCAM). IEEE Press, September 2006. (DOI, acm portal)
  • Matthew Hoosier, Matthew B. Dwyer, Robby, and John Hatcliff, "A Case Study in Domain-Customized Model Checking for Real-Time Component Software", Proceedings of the 2004 International Symposium on Leveraging Applications in Formal Methods (ISOLA 2004), Paphos, Cyprus, Lecture Notes in Computer Science (4313), pp. 161–180. (DOI, acm portal)
  • Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Ranganath, Robby, and Todd Wallentine, "Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs", Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2006), Vienna, Austria, March, 2006, Lecture Notes in Computer Science (3920), pp. 73 – 89. (.pdf)
  • Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, and John Hatcliff. "A New Foundation For Control-Dependence and Slicing for Modern Program Structures", Proceedings of the European Symposium On Programming (ESOP’05), Edinburg, Scotland, April 2005, Lecture Notes in Computer Science (3444), pp. 77–93. (DOI, acm portal)
  • Ganeshan Jayaraman, Venkatesh Prasad Ranganath, and John Hatcliff. "Kaveri: Delivering Indus Java Program Slicer to Eclipse", Proceedings of the International Symposium on Fundamental Approaches to Software Engineering (FASE’05) Edinburg, Scotland, April 2005, Lecture Notes in Computer Science (3442), pp. 269–272. (.pdf, .ps)
  • Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby. "Building Your Own Software Model Checker Using The Bogor Extensible Model Checking Framework", Proceedings of 17th Conference on Computer-Aided Verification (CAV 2005), Edinburgh, Scotland, July 2005, Lecture Notes in Computer Science (3576), pp. 148–152. (.pdf)
  • Edwin Rodrguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby. "Extending JML for Modular Specification and Verification of Multi-Threaded Programs", Proceedings of 19th European Conference on Object-Oriented Programming (ECOOP 2005), Glasgow, Scotland, July 2005, Lecture Notes in Computer Science (3586), pp. 148–152. (.pdf)
  • Robby, Edwin Rodriguez, Matthew Dwyer, and John Hatcliff, "Checking Strong Specifications Using an Extensible Software Model-checking Framework", Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems, April, 2004. Lecture Notes in Computer Science (2988), pp. 404–420. (DOI, acm portal)
  • John Hatcliff, William Deng, Matthew Dwyer, Masaaki Mizuno, "SyncGen : An Aspect-oriented Framework for Automatically Generating Synchronization Implementations from High-level Specifications", Proceedings of the International Conference on Tool and Algorithms for Construction and Analysis of Systems, April, 2004. Lecture Notes in Computer Science (2988), pp. 158–162. (coming soon)
  • Georg Jung, John Hatcliff, and Venkatesh Ranganath, "An Event Correlation Framework for the CORBA Component Model", Proceedings of the International Conference on Fundamental Aspects of Software Engineering, April, 2004. Lecture Notes in Computer Science (2984), pp. 144–159. (DOI, acm portal)
  • Adam Childs, Jesse Greenwald, Venkatesh Ranganath, Xinhua Deng, Matthew Dwyer, John Hatcliff, Georg Jung, Prashant Shanti Kumar, Gurdip Singh, "Cadena : An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-based Systems", Proceedings of the International Conference on Fundamental Aspects of Software Engineering, April, 2004. Lecture Notes in Computer Science (2984), pp. 160–164. (acm portal)
  • Venkatesh Ranganath and John Hatcliff, "Pruning Interference and Ready Dependence the Slicing Concurrent Java Programs", Proceedings of the International Conference on Compiler Construction, April, 2004. Lecture Notes in Computer Science (2985), pp. 39–56. (.pdf)
  • Edwin Rodrguez, Matthew B. Dwyer, John Hatcliff, Robby. "A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking", Proceedings of the 2004 International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), June 2004. Lecture Notes in Computer Science. (DOI, acm portal)
  • John Hatcliff, Robby, and Matthew Dwyer, "Verifying Atomicity Specifications for Concurrent Object-Oriented Software using Model-Checking", Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation, Venice, Italy. January, 2004. (pdf)
  • Matthew Dwyer, Robby, John Hatcliff, and Xinhua Deng, "Space Reductions for Model Checking Quasi-cyclic Systems", Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003), Lecture Notes in Computer Science, Springer-Verlag, Oct., 2003. (pdf [updated: July 28, 2003], case-studies)
  • Robby, Matthew B. Dwyer, John Hatcliff. "Bogor: An Extensible and Highly-Modular Model Checking Framework", Proceedings of the 2003 ACM Conference on Foundations of Software Engineering. Helsinki, Finland, September 2003. (pdf[updated: July 1, 2003], DOI, acm portal).
  • Robby, Matthew Dwyer, John Hatcliff,and Radu Iosif. "Space-Reduction Strategies for Model Checking Dynamic Software", in Proceedings of the 2nd Workshop on Software Model Checking, Electronic Notes in Computer Science, 89.3, June, 2003. (.pdf)
  • William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh. "Model-checking Middleware-based Event-driven Real-time Embedded Software", Proceedings of the 2002 International Conference on Formal Methods for Components and Objects (FMCO 2002). Leiden, The Netherlands, November 2002 (invited paper). (.pdf[updated: April 9, 2003], DOI, acm portal)
  • John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Ranganath, and Robby. "Slicing and Partial Evaluation of CORBA Component Model Designs for Avionics Systems", in Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, June, 2003. (DOI, acm portal)
  • John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad. "Cadena: An Integrated Development, Analysis, and Verification Environment for Componentbased Systems", Proceedings of the International Conference on Software Engineering (ICSE 2003). IEEE Press. Portland, Oregon, May 2003. (.pdf)
  • Xianghua Deng, Matthew B. Dwyer, John Hatcliff, and Masaaki Mizuno. "Invariant-based Specification, Synthesis, and Verification of Synchronization in Concurrent Programs", Proceedings of International Conference on Software Engineering (ICSE 2002), IEEE Press, May 2002. (DOI, acm portal)
  • John Hatcliff and Matthew Dwyer. "Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software", Proceedings of 12th International Conference on Concurrency Theory (CONCUR 2001), August 2001, LNCS 2154, Springer-Verlag, pp. 39 – 58 (invited paper). (abstract, .ps.gz) Warning: the uncompressed postscript version is ~3 MB due to multiple screen images.
  • Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng. "Tool-supported Program Abstraction for Finite-state Verification", Proceedings of the Internation Conference on Software Engineering (ICSE 2001), May 2001, IEEE Press. (abstract, .ps.gz)
  • James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, Hongjun Zheng. "Bandera : Extracting Finite-state Models from Java Source Code", Proceedings of the Internation Conference on Software Engineering (ICSE 2000), May 2000, IEEE Press. (abstract, .ps.gz,DOI, acm portal)
  • James Corbett, Matthew Dwyer, John Hatcliff, Robby, "A Language Framework For Expressing Checkable Properties of Dynamic Software", Proceedings of the 2000 Spin Workshop. August, 2000. Stanford, CA, USA. LNCS 1885, pp. 205 – 223. (.ps.gz, abstract, acm portal)
  • John Hatcliff, Matthew B. Dwyer. "Slicing Software for Model Construction", Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. (DOI, acm portal)
  • John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hognjun Zheng, "A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives", Proceedings of the International Symposium on Static Analysis (SAS’99). Venice, Italy, September, 1999, LNCS 1694, pp. 1– 18. (abstract, .ps.gz, acm portal)
  • John Hatcliff, Matthew Dwyer, Shawn Laubach. "Staging Static Analyses Using Abstraction-based Program Specialization", Proceedings of the 1998 Symposium on Programming Languages, Implementations, Logics and Programs (PLILP’98). Pisa, Italy, September, 1998. LNCS 1490, pp. 134 – 151. ( abstract, .ps.gz,acm portal)
  • Hatcliff, John. "Introduction to Partial Evalutation Using a Simple Flowchart Language", Proceedings of the DIKU 1998 International Summerschool on Partial Evaluation. LNCS 1706. (acm portal)
  • Gilles Barthe, John Hatcliff, and Peter Thiemann, "Monadic Type Systems: Pure Type Systems for Impure Settings", Proceedings of the Second HOOTS Workshop (editors A. Gordon and A. Pitts and C. Talcott), Stanford University, Palo Alto, CA. December, 1997. Electronic Notes in Computer Science, Volume 10. (abstract, .ps.gz)
  • Gilles Barthe, John Hatcliff, Morten Heine Soerensen, "Reflections on Reflections", Proceedings of the Ninth International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP’97), (editors H. Glaser, P. Hartel, and H. Kuchen) Pisa, Italy, September, 1997. LNCS 1292, pp. 241 – 258. (abstract, .ps.gz, .ps.gz[extended version], acm portal)
  • Gilles Barthe, John Hatcliff, Morten Heine Soerensen, "An Approach to Classical Pure Type Systems", Proceedings of The Thirteenth Annual Conference on Mathematical Foundations of Programming Language Semantics (MFPS XIII) (S. Brookes and M. Mislove, editors), Pittsburgh, PA, March, 1997. Electronic Notes and Theoretical Computer Science, Volume 6. (coming soon)
  • John Hatcliff and Robert Glück, "Reasoning about Hierarchies of Online Specialization Systems", Proceedings of the Dagstuhl Seminar on Partial Evaluation, February 1996, pp. 161–182. LNCS 1110. (acm portal)
  • Robert Glück, John Hatcliff, and Jesper Joergensen, "Generalization in Hierarchies of Online Program Specialization Systems", Proceedings of 1999 Conference on Logic-Based Program Synthesis and Transformation (P. Flener, editor), pp. 197–198. LNCS 1559. (acm portal)
  • John Hatcliff, "Mechanically Verifying the Correctness of an Off-line Partial Evaluator," Proceedings of the Seventh International Symposium on Programming Languages, Implementations, Logics and Programs, Utrecht, The Netherlands. September, 1995. Lecture Notes in Computer Science, Number 982. (plilp95.dvi.gz, plilp95.ps.gz, offline-pe.tar.gz[associated Elf implementation], acm portal) Extended version appears as DIKU tech report 95/14.
  • John Hatcliff and Olivier Danvy, "A Generic Account of Continuation-Passing Styles," Proceedings of the 21st annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, 1994. (agaocps-popl94.dvi.Z, DOI, acm portal).
  • Olivier Danvy and John Hatcliff, "On the Transformation between Direct and Continuation Semantics," Proceedings of the 9th Conference on Mathematical Foundations of Programming Semantics, New Orleans, April 1993. Lecture Notes in Computer Science, Number 802. (mfps93.ps.Z, acm portal)