Research Directed by Gary T. Leavens

This page summarizes the research directed by Gary T. Leavens at the University of Central Florida in the Department of Computer Science. (Research prior to July 2007 took place at Iowa State University, in the Department of Computer Science.) An up-to-date copy is available on the world wide web in the following URL.

 http://www.cs.ucf.edu/~leavens/main.html

Also on-line is a a list of my students and former students with their research. You can also download a BibTeX file with entries for all my papers. See also the section below on how to get the papers mentioned. Note: if you are not able to download the ACM papers for free (you see "unauthorized link specified" under the ACM authorized papers), then please reload this page using the link http://www.cs.ucf.edu/~leavens/main.html.

You might also want to look in my home page, where there is:

• a general description of my research,
• a short list of representative publications, and
• a list of my other WWW pages.

Specification and Formal Methods

General

CS-TR-15-01 defines a fine-grained region logic with conditional effects.

CS-TR-13-02 explores the relationship between separation logic, region logic, and dynamic frames theory. However it is obsolete and will be replaced.

CS-TR-09-01 is a survey of behavioral interface specification languages.

Information hiding and visibility of specification constructs is the focus of TR06-28.

A roadmap for research related to verified software is found in TR06-21.

The ACL approach to preventing aliasing from repeated parameters is described in TR98-08a and the C/ACL compiler is described in TR01-11.

Ownership applied to specifications is the topic of several papers. TR02-02a (an expansion of TR01-03) describes an application of Peter Müller's dissertation work on modular specification of frame properties to JML. This is also the basis for the work on modular invariants.

Specification of superclasses to allow work on subclasses is the topic of TR #00-05 with Clyde Ruby; it describes a technique for reasoning about the correctness of subclasses.

The execution of specifications in the context of the language SPECS-C++ is the subject of TR #00-02, TR #97-12a, and TR #94-02b with Tim Wahls.

A translation of Z specifications into Larch is the subject of Hua Zhong's master's project.

Various specification enhancements found in Larch/C++ are described in TR #97-19.

Inheritance of specifications in an object-oriented context is discussed in a WIDL paper. This topic was further developed in an ICSE 1996 paper with Krishna Kishore Dhara (see below).

(See also the Larch FAQ and the work on JML.)

• Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Unifying separation logic and region logic to allow interoperability. Formal Aspects of Computing, online May 2018. https://rdcu.be/PgJW
• ACM DL Author-ize serviceReasoning tradeoffs in languages with enhanced modularity features

  José Sánchez, Gary T. Leavens
  MODULARITY 2016 Proceedings of the 15th International Conference on Modularity, 2016
  [フレーム]
• Hridesh Rajan, Tien N. Nguyen, Gary T. Leavens, and Robert Dyer. Inferring behavioral specifications from large-scale repositories by leveraging collective intelligence. In Proceedings of the 37th International Conference on Software Engineering (ICSE'15) - Volume 2, Florence, Italy, pages 579-582. IEEE Press, May 2015.
• ACM DL Author-ize serviceConditional effects in fine-grained region logic

  Yuyan Bao, Gary T. Leavens, Gidon Ernst
  FTfJP '15 Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, 2015
  [フレーム]
• Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Translating Separation Logic into Dynamic Frames Using Fine-Grained Region Logic. Computer Science, University of Central Florida, CS-TR-13-02a, March 2014. [abstract] [Preprint PDF]
• José Sánchez and Gary T. Leavens. Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification. In Software Composition: 12th International Conference, SC 2013, Budapest, Hungary, June 2013, Proceedings, Springer-Verlag, Lecture Notes in Computer Science, Vol. 8088, pages 65-80. The original publication is available at link.springer.com from http://dx.doi.org/10.1007/978-3-642-39614-4_5.
• Ghaith Haddad and Gary T. Leavens. Specifying Subtypes in Safety Critical Java Programs. Concurrency and Computation Practice and Experience, 25(16):2290-2306. John Wiley & Sons, Ltd., Nov. 2013. http://dx.doi.org/10.1002/cpe.2930.
  Also Dept. of Computer Science, University of Central Florida, CS-TR-11-04, July 2011. [Preprint PDF]
• ACM DL Author-ize serviceSpecifying subtypes in SCJ programs

  Ghaith Haddad, Gary T. Leavens
  JTRES '11 Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, 2011, pp. 40-46.
  [フレーム]
• Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiß. The 1st Verified Software Competition: Experience Report. In Michael Butler and Wolfram Schulte (eds.), FM'11: Proceedings of the 17th international conference on Formal methods, pages 154-168. Volume 6664 of Lecture Notes in Computer Science, Springer-Verlag, 1999. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/978-3-642-21437-0_14.
• ACM DL Author-ize serviceOn the interplay of exception handling and design by contract: an aspect-oriented recovery approach

  Henrique Rebêlo, Roberta Coelho, Ricardo Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota, Fernando Castor
  FTfJP '11 Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, 2011, pp. 7:1-7:6.
  [フレーム]
• ACM DL Author-ize serviceThe design of SafeJML, a specification language for SCJ with support for WCET specification

  Ghaith Haddad, Faraz Hussain, Gary T. Leavens
  JTRES '10 Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, 2010, pp. 155-163.
  [フレーム]
• ACM DL Author-ize serviceChallenge benchmarks for verification of real-time programs

  Tomas Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, Jan Vitek
  PLPV '10 Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification, 2010, pp. 57-62.
  [フレーム]
• ACM DL Author-ize serviceThe future of library specification

  Gary T. Leavens
  FoSER '10 Proceedings of the FSE/SDP workshop on Future of software engineering research, 2010, pp. 211-215.
  [フレーム]
  Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-10-09, Aug 2010. [TR abstract] [TR PDF]
• Gary T. Leavens, Peter O'Hearn, and Sriram K. Rajamani (editors). Verified Software: Theories, Tools, Experiments: Third International Conference, VSTTE 2010, Edinburgh, UK, August 2010, Proceedings, Volume 6217 of Lecture Notes in Computer Science, Springer-Verlag, 2010. The original publication is available at springerlink.com [PDF]
• ACM DL Author-ize serviceThe verified software initiative: A manifesto

  C.A.R. Hoare, Jayadev Misra, Gary T. Leavens, Natarajan Shankar
  ACM Computing Surveys (CSUR), 41(4):22:1-22:8, October 2009
  [フレーム]
• Hridesh Rajan, Jia Tao, Steve Shaner, and Gary T. Leavens. Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. In Giuseppe Castagna (ed.), Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, pages 333-347, March 2009. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/978-3-642-00590-9_24.
  See also Department of Computer Science, Iowa State University, TR #08-07, July 2008. [TR abstract] [TR PDF]
• ACM DL Author-ize serviceBehavioral interface specification languages

  John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew Parkinson
  ACM Computing Surveys, 44(3):16:1-16:58, June, 2012.
  [フレーム]
  Also Dept. of EECS, University of Central Florida, CS-TR-09-01, March 2009. [abstract] [PDF] [Survey home] [Examples]
• Gary T. Leavens and Peter Müller. Information Hiding and Visibility in Interface Specifications. In ICSE 2007, May 2007, pages 385-395. [DOI: 10.1109/ICSE.2007.44]
  Also Department of Computer Science, Iowa State University, TR #06-28, September 2006. [abstract] [Preprint PDF] [Preprint PostScript]
• ACM DL Author-ize serviceRoadmap for enhanced languages and methods to aid verification

  Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump
  In Fifth International Conference on Generative Programming and Component Engineering (GPCE), pages 221-235, ACM, October 2006.
  [フレーム]
• Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 19(2):159--189, June 2007. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/s00165-007-0026-7.
  Also Department of Computer Science, Iowa State University, TR #06-14a, May 2006, revised August 2006. [abstract] [Preprint PDF] [Preprint PS]
• Yoonsik Cheon, Yoshiki Hayashi, and Gary T. Leavens. A Thought on Specification Reflection. Department of Computer Science, Iowa State University, TR #03-16, December 2003. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Invariants for Object Structures. ETH Zurich, Technical Report 424, October 2003. [abstract] [PDF]
• Gregory W. Kulczycki, Murali Sitaraman, William F. Ogden, and Gary T. Leavens. Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction. Department of Computer Science, Iowa State University, TR #02-13a, December 2002, revised December 2003. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117-154, February, 2003.
  Also Department of Computer Science, Iowa State University, TR #02-02a, February 2002, revised October 2002. [abstract] [postscript] [PDF]
• Medhat G. Assaad and Gary T. Leavens. Alias-free parameters in C for Better Reasoning and Optimization. Department of Computer Science, Iowa State University, TR #01-11, November 2001. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. In the Formal Techniques for Java Programs 2001, workshop at ECOOP 2001.
  Also Department of Computer Science, Iowa State University, TR #01-03, April 2001. [abstract] [postscript] [PDF]
• ACM DL Author-ize serviceFormal semantics of an algorithm for translating model-based specifications to concurrent constraint programs

  Tim Wahls, Gary T. Leavens
  SAC '01 Proceedings of the 2001 ACM symposium on Applied computing, 2001, pp. 567-575.
  [フレーム]
• ACM DL Author-ize serviceSafely creating correct subclasses without seeing superclass code

  Clyde Ruby, Gary T. Leavens
  OOPSLA '00 Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, 2000, pages 208-228.
  [フレーム]
• Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing Formal Specifications with Concurrent Constraint Programming. Automated Software Engineering, 7(4):315-343, December, 2000.
  Also Department of Computer Science, Iowa State University, TR #97-12c, August 1997, revised June 1998, May, July 2000. [abstract] [postscript]
• Tim Wahls and Gary T. Leavens. Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs. Department of Computer Science, Iowa State University, TR #00-02a, March 2000, revised August 2000. [abstract] [postscript]
• Gary T. Leavens and Olga Antropova. ACL -- Eliminating Parameter Aliasing with Dynamic Dispatch. Department of Computer Science, Iowa State University, TR #98-08a, July 1998, revised February 1999. [abstract] [postscript]
• Hua Zhong. LSL Traits for using Z with Larch. Department of Computer Science, Iowa State University, TR #97-22, December 1997. [abstract] [postscript]
• Gary T. Leavens and Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. In Jeannette M. Wing, James Woodcock, and Jim Davies (editors). FM'99 -- Formal Methods: World Congress on Formal Methods in Development of Computer Systems, Toulouse, France, September 1999, pages 1087-1106. Volume 1709 of Lecture Notes in Computer Science, Springer-Verlag, 1999. http://www.springerlink.com/content/74v251avr98krlmw
  Also: Department of Computer Science, Iowa State University, TR #97-19b, September 1997, revised February, June 1999.
• Gary T. Leavens and Clyde Ruby. Specification Facets for More Precise, Focused Documentation. In the Proceedings of the Eighth Annual Workshop on Software Reuse (WISR8), Columbus Ohio, March 1997.
  Also Department of Computer Science, Iowa State University, TR #97-04, January 1997. [abstract] [postscript]
• Gary T. Leavens and Jeannette M. Wing. Protective Interface Specifications. Formal Aspects of Computing, 10(1):59-75, January 1998. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/PL00003926.
  An earlier version appears in Michel Bidoit and Max Dauchet (editors), TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, pages 520-534. Volume 1214 of Lecture Notes in Computer Science, Springer-Verlag, 1997.
• Tim Wahls, Albert L. Baker, and Gary T. Leavens. The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes. Department of Computer Science, Iowa State University, TR #94-02b, February 1994, revised November 1994. [abstract] [PDF] [postscript]
• ACM DL Author-ize serviceInheritance of interface specifications (extended abstract)

  Gary T. Leavens
  IDL '94 Proceedings of the workshop on Interface definition languages, 1994, pp. 129-138.
  [フレーム]
• Gary T. Leavens and Yoonsik Cheon. Overview and Specification of the Built-in Types in Little Smalltalk. Department of Computer Science, Iowa State University, TR #91-22a, October 1991, revised February 1994. [abstract] [PDF]
• ACM DL Author-ize serviceFormal techniques for OO software development

  Pierre America, Derek Coleman, Roger Duke, Doug Lea, Gary Leavens
  OOPSLA '91 Conference proceedings on Object-oriented programming systems, languages, and applications, 1991, pp. 166-170.
  [フレーム]

The JML Project

JML is a behavioral interface specification language tailored to the specification of Java modules. It combines the approaches of Eiffel and Larch, with some elements of the refinement calculus. Its home page is

 http://www.jmlspecs.org/

The Larch/C++ Project

Larch/C++ is a behavioral interface specification language tailored to the specification of C++ modules. Its home page is

 http://www.cs.ucf.edu/~leavens/larchc++.html

Larch/Smalltalk

Larch/Smalltalk is a behavioral interface specification language tailored to the specification of Smalltalk modules. Its home page is

 http://www.cs.ucf.edu/~leavens/larchSmalltalk.html

Yoonsik Cheon is the main designer of Larch/Smalltalk.

Larch/CORBA

The following paper gives the idea of designing Larch/CORBA, a behavioral interface specification language tailored to OMG's IDL.

• Gary T. Leavens and Yoonsik Cheon. Extending CORBA IDL to Specify Behavior with Larch. In OOPSLA '93 Workshop Proceedings: Specification of Behavioral Semantics in OO Information Modeling, pages 77-80. (Also Department of Computer Science, Iowa State University, TR #93-20, August 1993. [abstract] [text file])

More useful is the master's thesis of Gowri Sankar Sivaprasad, which gives a design of Larch/CORBA.

• Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of CORBA-IDL Interfaces. Department of Computer Science, Iowa State University, TR #95-27a, December 1995, revised December 1995. [abstract] [PDF]

Semantics

An introductory survey of class-based and algebraic models of objects that may be read as background to the rest of these is the following.

• Gary T. Leavens and Don Pigozzi. Class-Based and Algebraic Models of Objects. In Rance Cleaveland and Michael Mislove and Philip Mulry (eds.), US---Brazil Joint Workshops on the Formal Foundations of Software Systems, Electronic Notes in Theoretical Computer Science, vol. 14 [abstract]

Model Theory for ADTs

The following is recent work by Don Pigozzi, Krishna Kishore Dhara and myself on model theory of behavior for ADTs. It is used to study subtyping in TR96-15.

• Gary T. Leavens and Don Pigozzi. The Behavior-Realization Adjunction and Generalized Homomorphic Relations. Theoretical Computer Science, 177:183-216, 1997.
  A slightly extended version is Department of Computer Science, Iowa State University, TR #94-18b, September 1994, revised September 1994, July 1996. [abstract] [PDF]
• Gary T. Leavens and Krishna Kishore Dhara. Blended Algebraic and Denotational Semantics for ADT Languages with Mutable Objects. Department of Computer Science, Iowa State University, TR #93-21b, September 1993, revised March, September 1994. [abstract] [PDF]

Behavioral Subtyping

Types with Mutable Objects

An overview that ties together the ideas of supertype abstraction, behavioral subtyping, and specification inheritance is found in the August 2015 artice in ACM TOPLAS. A presentation of these ideas in the context of JML is found in TR#06-22.

For historical perspective, see the survey of behavioral subtyping in the Foundations of Component-Based Systems book.

Work with Krishna Kishore Dhara on subtyping concerns types with mutable objects is listed in this subsection. The most recent work with Dhara is TR #01-02, which has a good explanation of the ideas. More detailed is his dissertation.

A shorter introduction to the idea of behavioral subtyping that may be more accessible is the ICSE 1996 paper (which appears with a correction as TR #95-20c). This paper describes the idea of specification inheritance and how it relates to behavioral subtyping. Its ideas were embodied in Larch/C++ and JML.

Also, note that TR #94-21b makes the following older TRs obsolete: TR #92-36 and TR #92-35. The work described in this part does not (yet) describe a specification language or a verification logic. Kishore's master's thesis can be had by requesting it by e-mail, but it is summarized in TR #92-36.

• ACM DL Author-ize serviceBehavioral Subtyping, Specification Inheritance, and Modular Reasoning

  Gary T. Leavens, David A. Naumann
  ACM Transactions on Programming Languages and Systems (TOPLAS), 2015
  [フレーム]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Computer Science, University of Central Florida, CS-TR-13-03a, July, 2013. [abstract] [PDF]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs. Department of Computer Science, Iowa State University, TR #06-36, December 2006. [abstract] [PDF] [postscript]
• Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. In Zhiming Liu and He Jifeng (eds), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Macao, China, pages 2-34. Volume 4260 of Lecture Notes in Computer Science , Springer-Verlag, 2006.
  Also Department of Computer Science, Iowa State University, TR #06-22, August 2006. [abstract] [postscript] [PDF]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Department of Computer Science, Iowa State University, TR #06-20b, July 2006, revised August, September 2006. [abstract] [postscript] [PDF]
• Krishna Kishore Dhara and Gary T. Leavens. Preventing Cross-Type Aliasing for More Practical Reasoning. Department of Computer Science, Iowa State University, TR #01-02a, March 2001, revised November 2001. [abstract] [postscript] [PDF]
• Gary T. Leavens and Krishna Kishore Dhara. Concepts of Behavioral Subtyping and a Sketch of Their Extension to Component-Based Systems. In Gary T. Leavens and Murali Sitaraman (eds.), Foundations of Component-Based Systems, chapter 6, pages 113-135. Cambridge University Press, New York, NY, 2000. [PDF], [postscript]
• Krishna Kishore Dhara. Behavioral Subtyping in Object-Oriented Languages. Department of Computer Science, Iowa State University, TR #97-09, May 1997. [abstract] [PDF] (117 pages).
• Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE, 1996.
  An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #95-20c, August 1995, revised August and December 1995, March 1997. [abstract] [PDF] [postscript]
• Krishna Kishore Dhara and Gary T. Leavens. Weak Behavioral Subtyping for Types with Mutable Objects. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, Preliminary Proceedings, pages 269-290.
  The final version appears in S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Volume 1 of Electronic Notes in Theoretical Computer Science, Elsevier, 1995.

Types with Immutable Objects

The IEEE Software and OOPSLA/ECOOP '90 papers are short summaries of this work. The MFPS paper with Don Pigozzi is also fairly short, and extends the results to higher types; it isolates the key mathematical idea. A development of this mathematical idea, which gives both a necessary and sufficient model-theoretic criterion for correct behavioral subtyping is found in TR96-15. The proof theory is studied in TR02-07.

• Gary T. Leavens and Don Pigozzi. Equational Reasoning with Subtypes. Department of Computer Science, Iowa State University, TR #02-07, July 2002. [abstract] [postscript] [PDF]
• Gary T. Leavens and Don Pigozzi. A Complete Algebraic Characterization of Behavioral Subtyping. Acta Informatica 36:617-663, 2000.
• Gary T. Leavens and William E. Weihl. Specification and Verification of Object-Oriented Programs Using Supertype Abstraction. Acta Informatica 32(8):705-778, November 1995. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/BF01178658.
  
  A longer version of this paper is Gary T. Leavens and William E. Weihl. Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs. Department of Computer Science, Iowa State University, TR #92-28d, September 1992, revised September and October 1993, and January and September 1994. [abstract] [PDF]
• Gary T. Leavens and Don Pigozzi. Typed Homomorphic Relations Extended with Subtypes. In Stephen Brookes, editor, Mathematical Foundations of Programming Semantics '91, pages 144-167. Volume 598 of Lecture Notes in Computer Science . Springer-Verlag, 1992. [SpringerLink]
• Gary T. Leavens. Modular Specification and Verification of Object-Oriented Programs. IEEE Software, 8(4):72-80, July, 1991. http://doi.ieeecomputersociety.org/10.1109/52.300040
• ACM DL Author-ize serviceReasoning about object-oriented programs that use subtypes

  Gary T. Leavens, William E. Weihl
  OOPSLA/ECOOP '90 Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, 1990, pp 212-223.
  [フレーム]
• Gary T. Leavens. Modular Verification of Object-Oriented Programs with Subtypes. Department of Computer Science, Iowa State University, TR #90-09, July 1990. [abstract] [PDF]
• Gary T. Leavens, Verifying Object-Oriented Programs that use Subtypes. Massachusetts Institute of Technology, Laboratory for Computer Science, Technical Report TR-439, February 1989.

The last report mentioned above, MIT/LCS/TR-439, is my Ph.D. dissertation. To get it, check your library, or write to Publications, Laboratory for Computer Science, Massachusetts Institute of Technology, 545 Technology Sq., Cambridge, MA 02139. Their phone number is (617)253-5894. The cost was 16ドル.00 US. But you probably don't need to do that, as the thesis was reworked in a different framework in ISU TR #90-09. The Acta Informatica paper is a summary of the thesis work; TR #92-28d contains that paper and additional omitted details.

Semantics of DFDs and their Execution

The first of the papers below, makes the second obsolete.

• ACM DL Author-ize serviceFormal semantics for SA style data flow diagram specification languages

  Gary T. Leavens, Tim Wahls, Albert L. Baker
  SAC '99 Proceedings of the 1999 ACM symposium on Applied computing, San Antonio, February/March, 1999, pages 526-532.
  [フレーム]
• Gary T. Leavens, Tim Wahls, Albert L. Baker, and Kari Lyle. An Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams. Department of Computer Science, Iowa State University, TR #93-28d, December 1993, revised December 1993, September 1994, June 1996, July 1996. [abstract] [PDF] [postscript]
• Tim Wahls, Albert L. Baker, and Gary T. Leavens, An Executable Semantics for a Formalized Data Flow Diagram Specification Language. Department of Computer Science, Iowa State University, TR #93-27, November 1993. [abstract] [PDF]

Other Papers on Semantics

A summary of the talks given at the workshop Foundations of Object-Oriented Languages (Paris, July 1994) is available in the following.

• Giuseppe Castagna and Gary T. Leavens. Foundations of Object-Oriented Languages: 2nd Workshop report. Department of Computer Science, Iowa State University, TR #94-22, November 1994. [abstract] [PDF]

Programming Language Design

Context-Oriented Programming

• ACM DL Author-ize serviceTowards Modular Reasoning for Context-Oriented Programs

  Tomoyuki Aotani, Gary T. Leavens
  FTfJP'16 Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, 2016
  [フレーム]

Aspect-Oriented Programming

See the page on More Modular Reasoning for Aspect-Oriented Programs for papers by Curtis Clifton, myself, and others related to aspect-oriented programming.

• ACM DL Author-ize serviceModularizing crosscutting concerns with ptolemy

  Hridesh Rajan, Sean Mooney, Gary T. Leavens, Robert Dyer, Rex D. Fernando, Mohammad Ali Darvish Darab, Bryan Welter
  SPLASH '11 companion, 2011, pp. 31-32.
  [フレーム]
• ACM DL Author-ize serviceTranslucid contracts: expressive specification and modular verification for aspect-oriented interfaces

  Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, Sean Mooney
  AOSD '11 Proceedings of the tenth international conference on Aspect-oriented software development, 2011, pp. 141-162.
  [フレーム]
• ACM DL Author-ize serviceModularizing crosscutting concerns with Ptolemy

  Hridesh Rajan, Gary T. Leavens, Robert Dyer, Mehdi Bagherzadeh
  AOSD '11 Proceedings of the tenth international conference on Aspect-oriented software development companion, 2011, pp. 61-62.
  [フレーム]
• ACM DL Author-ize serviceApplying translucid contracts for modular reasoning about aspect and object oriented events

  Mehdi Bagherzadeh, Gary T. Leavens, Robert Dyer
  FOAL '11 Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, 2011, pp. 31-35.
  [フレーム]
• ACM DL Author-ize serviceTranslucid contracts for modular reasoning about aspect-oriented programs

  Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, Sean Mooney
  SPLASH '10 Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, 2010, pp. 245-246.
  [フレーム]
• ACM DL Author-ize serviceMultiple concerns in aspect-oriented language design: a language engineering approach to balancing benefits, with examples

  Gary T. Leavens, Curtis Clifton
  SPLAT '07 Proceedings of the 5th workshop on Software engineering properties of languages and aspect technologies, 2007, article 6.
  [フレーム]
  Also Department of Computer Science, Iowa State University, TR #07-01a, February 2007. [abstract] [PDF] [PS]

The MultiJava Project

MultiJava is an extension to Java that supports modular open classes and multiple dispatch. See the MultiJava publications page for other papers on MultiJava.

• ACM DL Author-ize serviceMultiJava: Design rationale, compiler implementation, and applications

  Curtis Clifton, Todd Millstein, Gary T. Leavens, Craig Chambers
  ACM TOPLAS, 28(3):517-575, May, 2006.
  [フレーム]
• ACM DL Author-ize serviceMultiJava: modular open classes and symmetric multiple dispatch for Java

  Curtis Clifton, Gary T. Leavens, Craig Chambers, Todd Millstein
  OOPSLA '00 Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, 2000, pages 130-145.
  [フレーム]

Papers on Type Systems

The two versions of ``A Type Notation for Scheme'' reflect an evolution of the type system, the report TR#05-18 is the latest of these.

• Gary T. Leavens, Curtis Clifton, and Brian Dorn. A Type Notation for Scheme. Department of Computer Science, Iowa State University, TR #05-18, August 2005. [abstract] [PDF] [postscript]
• Gary T. Leavens and Curtis Clifton. A Type Notation for Scheme. Department of Computer Science, Iowa State University, TR #05-03, February 2005. [abstract] [PDF] [postscript]
• Jianbing Chen. Dynamic Semantics and Type-checking of Tuple. Department of Computer Science, Iowa State University, TR #98-10, December 1998. [abstract] [postscript].
• ACM DL Author-ize serviceFormal methods for multimethod software components

  Gary T. Leavens
  ACM SIGSOFT Software Engineering Notes, 25(1):62-63, January, 2000.
  [フレーム]
• ACM DL Author-ize serviceMultiple dispatch as dispatch on Tuples

  Gary T. Leavens, Todd D. Millstein
  OOPSLA '98 Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, 1998, pages 374-387.
  [フレーム]
• Craig Chambers and Gary T. Leavens. BeCecil, A Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing. Presented at the The Fourth International Workshop on Foundations of Object-Oriented Languages FOOL 4, Paris, France.
  An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #96-17a, December 1996, revised April 1997. [abstract] [postscript (101 pages)]. The main body and just the appendix sections are also available.
• Steven Jenkins and Gary T. Leavens. Polymorphic Type-Checking in Scheme. Computer Languages, 22(4): 215-223, 1996.
  Also Department of Computer Science, Iowa State University, TR95-21a, August 1995, revised May 1996. [abstract] [PDF] [postscript]
• Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce. On Binary Methods. Theory and Practice of Object Systems 1(3):221-242, 1995.
  Also Department of Computer Science, Iowa State University, TR95-08a, May 1995, revised December 1995. [abstract] [PDF]
• Craig Chambers and Gary T. Leavens. Towards Safe Modular Extensible Objects. Department of Computer Science, Iowa State University, TR #94-17a, August 1994. [abstract] [PDF] [postscript]
• Craig Chambers and Gary T. Leavens. Typechecking and Modules for Multimethods. ACM Transactions on Programming Languages and Systems, 17(6):805-843, November 1995. http://doi.acm.org/10.1145/218570.218571
  The longer version (with an appendix of formal proofs) is Department of Computer Science, Iowa State University, TR #95-19, August 1995. [abstract] [PDF]
• ACM DL Author-ize serviceTypechecking and modules for multimethods

  Craig Chambers, Gary T. Leavens
  ACM Transactions on Programming Languages and Systems (TOPLAS), 17(6):805-843, 1995.
  [フレーム]
  A longer version (with formal proofs) is Department of Computer Science, Iowa State University, TR #94-03a, March 1994, revised August 1994. [abstract] [PDF]
• ACM DL Author-ize serviceTypechecking and modules for multi-methods

  Craig Chambers, Gary T. Leavens
  OOPSLA '94 Proceedings of the ninth annual conference on Object-oriented programming systems, language, and applications, 1994, pp. 1-15.
  [フレーム]

Other Papers on Programming Language Design

• Gary T. Leavens. Introduction to the Literature on Semantics. Department of Computer Science, Iowa State University, TR #94-15, August 1994. [abstract] [PDF]
• Gary T. Leavens. Introduction to the Literature On Programming Language Design. Department of Computer Science, Iowa State University, TR #93-01b, January 1993, revised January 1994 and February 1996. [abstract] [postscript]
• ACM DL Author-ize serviceIntroduction to the literature on object-oriented design, programming, and languages

  Gary T. Leavens
  ACM SIGPLAN OOPS Messenger, 2(4):40-53, October 1991
• Barbara Liskov, Mark Day, Maurice Herlihy, Paul Johnson, Gary T. Leavens (editor), Robert Scheifler, and William Weihl. Argus Reference Manual. Massachusetts Institute of Technology, Laboratory for Computer Science, Technical Report TR-400, October 1987. [postscipt]
• ACM DL Author-ize servicePrettyprinting styles for various languages

  Gary T. Leavens
  ACM SIGPLAN Notices, 19(2):75-79, February, 1984.
  [フレーム]

Other Papers

Teaching Computer Science

• ACM DL Author-ize serviceVerily: a web framework for creating more reasonable web applications

  John L. Singleton, Gary T. Leavens
  ICSE Companion 2014 Companion Proceedings of the 36th International Conference on Software Engineering, 2014
  [フレーム]
• ACM DL Author-ize serviceUse concurrent programming models to motivate teaching of programming languages

  Gary T. Leavens
  In Programming Languages Curriculum Workshop 2008, ACM SIGPLAN Notices, 43(11):93-98, Nov. 2008.
  [フレーム]
  Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-08-04a, April 2008, revised May 2008. [abstract] [Preprint PDF]
• ACM DL Author-ize serviceSIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations

  Eric Allen, Mark W. Bailey, Ras Bodik, Kim Bruce, Kathleen Fisher, Stephen Freund, Robert Harper, Chandra Krintz, Shriram Krishnamurthi, Jim Larus, Doug Lea, Gary Leavens, Lori Pollock, Stuart Reges, Martin Rinard, Mark Sheldon, Franklyn Turbak, Mitchell Wand
  ACM SIGPLAN Notices, 43(11):6-29, Nov. 2008.
  [フレーム]
• Gary T. Leavens. Following the Grammar. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-07-10c, September 2007, revised October, November 2007, October 2009. [abstract] [PDF] [postscript]
• Gary T. Leavens. Following the Grammar. Department of Computer Science, Iowa State University, TR #05-02a, February 2005, revised January 2006. [abstract] [PDF] [postscript]
• Gary T. Leavens, Albert L. Baker, Vasant Honavar, Steven M. LaValle, Gurpur Prabhu. Programming is Writing: Why Student Programs must be Carefully Evaluated. Mathematics and Computer Education, 32(3):284-295, Fall 1998.
• Gary T. Leavens. A Physical Example for Teaching Curried Functions. Mathematics and Computer Education, 30(1):51-60, Winter 1996.
• Gary T. Leavens. Aiding Self-motivation with Readings in Introductory Computing. Mathematics and Computer Education, 29(2):124-133, 1995.
• Albert L. Baker, David Fernandez-Baca, and Gary T. Leavens. Course Specifications for New Introductory Courses: Computer Science 227X and 228X. Department of Computer Science, Iowa State University, TR #92-09, April 1992. [abstract] [postscript]

The 3x+1 Problem

• Gary T. Leavens and Mike Vermeulen, 3x+1 Search Programs. Computers and Mathematics with Applications, 24(11):79-99, December 1992.
• Gary T. Leavens. A Distributed Search Program for the 3x+1 problem. Department of Computer Science, Iowa State University, TR #89-22, November 1989. [abstract] [PDF]

Miscellaneous

• Amirfarhad Nilzadeh, Wojciech Mazurczyk, Cliff Zou, and Gary T. Leavens. Information Hiding in RGB Images Using an Improved Matrix Pattern Approach. in The First International Workshop on The Bright and Dark Sides of Computer Vision: Challenges and Opportunities for Privacy and Security (CV-COPS 2017), workshop at CVPR, Honolulu, Hawii, July, 2017. [PDF]
• Rochelle Elva and Gary T. Leavens. JSCTracker: A Semantic Clone Detection Tool for Java Code. Dept. of EECS, University of Central Florida, CS-TR-12-04, March 2012. [abstract] [PDF]
• Kristina P. Boysen and Gary T. Leavens. Automatically generating consistent graphical user interfaces using a parser generator. Department of Computer Science, Iowa State University, TR #04-07a, August 2004, revised November 2005. [abstract] [PDF]
• ACM DL Author-ize service1997 workshop on foundations of component-based systems

  Gary T. Leavens, Oscar Nierstrasz, Murali Sitaraman
  ACM SIGSOFT Software Engineering Notes, 23(1):38-41, January, 1998
  [フレーム]
• Gary T. Leavens. Fields in Physics are like Curried Functions, or Physics for Functional Programmers. Department of Computer Science, Iowa State University, TR #94-06b, April 1994, revised May 1994. [abstract] [PDF]

How to get Papers Mentioned

Although it might violate the copyright laws, if you don't have a published paper in your library, you can probably get some version of it as a University of Central Florida or Iowa State University (ISU) Computer Science TR. (This is not to encourage you to violate the copyright law, however.) All ISU Com S TRs, including many old versions, should be available by the following means.

Through the web

You can get Computer Science TRs from the library's page at https://lib.dr.iastate.edu/cs_techreports/.

Contact Information

Last update $Date: 2023年10月02日 18:20:00 $