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:

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.)

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.

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

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.

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.

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.

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.

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.

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.

Programming Language Design

Context-Oriented Programming

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.

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.

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.

Other Papers on Programming Language Design

Other Papers

Teaching Computer Science

The 3x+1 Problem

Miscellaneous

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

Gary T. Leavens
University of Central Florida
College of Engineering and Computer Science
Dept. of Computer Science, Building 116
4000 Central Florida Blvd.,
Orlando, Florida 32816-2362 USA

e-mail: Leavens@ucf.edu
Phone: +1-407-823-4758 / fax: +1-407-823-5419

Last update $Date: 2023/10/02 18:20:00 $