Students of Gary T. Leavens

The following describes students whose research I am supervising or have supervised, and some information on their research and publications.

I have also collaborated with Todd Millstein, Vassily Litvinov, Peter Müller and Edwin Rodríguez at other Universities.

To all current and former co-authors: your Erdös number is no more than 5! You may also be interested in your (and my) academic genealogy.

Current Graduate Students

Kristina P. Boysen

(M.S.), Summer 2005--present.

• 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]

Neeraj Khanolkar

(M.S.), Summer 2005--present, joint with Prof. Soma Chadhuri.

• Neeraj Khanolkar and Gary T. Leavens. Executable Documentation of Template-Hook Interactions in Frameworks using JML. Department of Computer Science, Iowa State University, TR #06-18, June 2006. [abstract] [postscript] [PDF]

Clyde Ruby

(Ph.D.), Spring 1995--present.

• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, Volume 55, pages 185-205, Elsevier, 2005.
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (eds.), Formal Methods for Components and Objects, pages 262-284. Volume 2852 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2003.
  Also Department of Computer Science, Iowa State University, TR #03-04, March 2003. [abstract] [PDF] [PostScript]
• Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. In OOPSLA 2000 Conference Proceedings, pages 208-228. Volume 35, number 10 of ACM SIGPLAN Notices, October 2000.
  Also Department of Computer Science, Iowa State University, TR #00-05d, April 2000, revised April, June, July 2000. [abstract] [postscript] [PDF]
• Gary T. Leavens, K. Rustan M. Leino, Erik Poll. Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota. Copyright ACM, 2000.
  Also Department of Computer Science, Iowa State University, TR #00-15, August 2000. [abstract] [postscript] [PDF]
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design [postscript] [PDF]. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Business and Systems, chapter 12, pages 175-188. Copyright Kluwer, 1999. Used by permission.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. To appear in ACM SIGSOFT Software Engineering Notes.
  Also Department of Computer Science, Iowa State University, TR #98-06-rev29, January 2006. [abstract] [postscript] [PDF]
• 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] [PDF]

Steven Jenkins

(Ph.D.), Summer 1995--present.

Robert (Bob) Lavey

(M.S.), Spring 1994--present.

Steve Shaner

(M.S.), Spring 2005--present.

Current Undergraduate (REU and 491) Students

None at the moment.

Former Graduate Students and Finished Theses

These are listed in reverse cronological order, with an entry for each degree awarded.

Cui Ye

(M.S.), ``Improving JML's assignable clause analysis,'' Spring 2005--August 2006.

• Cui Ye. Improving JML's assignable clause analysis. Department of Computer Science, Iowa State University, TR #06-19-23, July 2006. [abstract] [PDF]

Curtis Clifton

(Ph.D), ``A design discipline and language features for modular reasoning in aspect-oriented programs,'' Spring 2002--July 2005.

• Curtis Clifton and Gary T. Leavens. A Design Discipline And Language Features For Modular Reasoning In Aspect-Oriented Programs. Department of Computer Science, Iowa State University, TR #05-23, December 2005. [abstract] [PDF] [PS]
• 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]
• Curtis Clifton. A design discipline and language features for modular reasoning in aspect-oriented programs. Department of Computer Science, Iowa State University, TR #05-15, July 2005. [abstract] [PDF]
• Gary T. Leavens and Curtis Clifton. Lessons from the JML Project. To appear in Verified Software: Theories, Tools, Experiments.
  Also Department of Computer Science, Iowa State University, TR #05-12a, April 2005, revised July 2005. [abstract] [PDF] [PostScript]
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, Volume 55, pages 185-205, Elsevier, 2005.
• Curtis Clifton, Todd Millstein, Gary T. Leavens, and Craig Chambers. MultiJava: Design Rationale, Compiler Implementation, and Applications. ACM TOPLAS, Volume 28, number 3 (May 2006), pages 517-575.
  Also Department of Computer Science, Iowa State University, TR #04-01b, January 2004, revised December 2004. [abstract] [PDF] [PostScript]
• Curtis Clifton, Gary T. Leavens and Mitchell Wand. Parameterized Aspect Calculus: A Core Calculus for the Direct Study of Aspect-Oriented Languages. Department of Computer Science, Iowa State University, TR #03-13, October 2003. [abstract] [PDF]
• Curtis Clifton, Gary T. Leavens and Mitchell Wand. Formal Definition of the Parameterized Aspect Calculus. Department of Computer Science, Iowa State University, TR #03-12, October 2003. [abstract] [PDF]
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (eds.), Formal Methods for Components and Objects, pages 262-284. Volume 2852 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2003.
  Also Department of Computer Science, Iowa State University, TR #03-04, March 2003. [abstract] [PDF] [PostScript]
• Curtis Clifton and Gary T. Leavens. Spectators and Assistants: Enabling Modular Aspect-Oriented Reasoning. Department of Computer Science, Iowa State University, TR #02-10, October 2002. [abstract] [PDF] [Postscript].
• Curtis Clifton and Gary T. Leavens Observers and Assistants: A Proposal for Modular Aspect-Oriented Reasoning. Department of Computer Science, Iowa State University, TR #02-04, March 2002. [abstract] [PDF].
• Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd Millstein. MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java. In OOPSLA 2000 Conference Proceedings, pages 130-145. Volume 35, number 10 of ACM SIGPLAN Notices, October 2000.
  Also Department of Computer Science, Iowa State University, TR #00-06a, April 2000, revised July 2000. [abstract] [postscript].

Brian J. Dorn

(M.S.), ``Design and implementation of a reusable type inference engine and its application to Scheme,'' Spring 2004--May 2005.

• 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]
• Brian J. Dorn. Design and implementation of a reusable type inference engine and its application to Scheme. Department of Computer Science, Iowa State University, TR #05-16, July 2005. [abstract] [PDF]

Tongjie Chen

(M.S.), ``Extending MultiJava with Generics,'' Fall 2000--Fall 2004.

Yoonsik Cheon

(Ph.D.), ``A Runtime Assertion Checker for the Java Modeling Language,'' Summer 1991--April 2003.

• Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, volume 7, number 3, pages 212-232, June 2005. [preprint PDF] (The original publication is available at http://www.springerlink.com.)
• Gary T. Leavens, Yoonsik Cheon, and David R. Cok. Demonstration of JML Tools. Department of Computer Science, Iowa State University, TR #05-13, April 2005. [abstract] [PDF] [PostScript]
• Yoonsik Cheon and Gary T. Leavens. A Contextual Interpretation of Undefinedness for Runtime Assertion Checking. To appear in AADEBUG 2005 Sixth International Symposium On Automated And Analysis-Driven Debugging, Monterey, California.
  Also Department of Computer Science, The University of Texas at El Paso, Technical Report #05-10, March 2005. [PDF]
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, Volume 55, pages 185-205, Elsevier, 2005.
• Yoonsik Cheon and Gary T. Leavens. The JML and JUnit Way of Unit Testing and its Implementation. Department of Computer Science, Iowa State University, TR #04-02a, February 2004, revised April 2004. [abstract] [postscript] [PDF]
• 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]
• Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model Variables: Cleanly Supporting Abstraction in Design By Contract. Department of Computer Science, Iowa State University, TR #03-10b, March 2003, revised September 2003, August 2004. [abstract] [PDF] [Postscript]
• Yoonsik Cheon. A Runtime Assertion Checker for the Java Modeling Language. Department of Computer Science, Iowa State University, TR #03-09, April 2003. [abstract] [PDF] [PostScript]
• Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications. Department of Computer Science, University of Nijmegen, NIII-R0309, Nijmegen, the Netherlands, March 2003. See http://www.cs.kun.nl/research/reports/. [PDF]
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (eds.), Formal Methods for Components and Objects, pages 262-284. Volume 2852 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2003.
  Also Department of Computer Science, Iowa State University, TR #03-04, March 2003. [abstract] [PDF] [PostScript]
• Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In Boris Magnusson (ed.), ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pages 231-255.
  Also Department of Computer Science, Iowa State University, TR #01-12a, November 2001, revised March 2002. [abstract] [postscript] [PDF]
• Yoonsik Cheon and Gary T. Leavens. A Runtime Assertion Checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun (eds.), International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada. CSREA Press, June 2002, pages 322-328.
  Also Department of Computer Science, Iowa State University, TR #02-05, March 2002. [abstract] [PDF]
• 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])
• 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] [postscript]
• Yoonsik Cheon and Gary T. Leavens. A Quick Overview of Larch/C++. Journal of Object-Oriented Programming, 7(6):39-49, October 1994.
• Gary T. Leavens and Yoonsik Cheon. Preliminary Design of Larch/C++. In U. Martin and J. Wing, editors, Proc. First International Workshop on Larch, Dedham 1992, pages 159-184. Workshops in Computing Series. Springer-Verlag, 1993.
• Yoonsik Cheon and Gary T. Leavens. A Gentle Introduction to Larch/Smalltalk Specification Browsers. Department of Computer Science, Iowa State University, TR #94-01, January 1994.
• Yoonsik Cheon and Gary T. Leavens. The Larch/Smalltalk Interface Specification Language. ACM Transactions on Software Engineering and Methodology, 3(3):221-253, July 1994.

Jeremiah S. (Jerry) Patterson

(M.S.), ``An Object-oriented Event Calculus,'' Fall 1999--Summer 2002.

• Jeremiah S. Patterson. An Object-Oriented Event Calculus. Department of Computer Science, Iowa State University, TR #02-08, July 2002. [abstract] [PDF] [Postscript].

Curtis Clifton

(M.S.), ``MultiJava: Design, implementation, and evaluation of a Java-compatible language supporting modular open classes and symmetric multiple dispatch,'' Spring 1998--Fall 2001.

• Curtis Clifton. MultiJava: Design, implementation, and evaluation of a Java-compatible language supporting modular open classes and symmetric multiple dispatch. Department of Computer Science, Iowa State University, TR #01-10, November 2001. [abstract] [PDF]

Medhat Assaad

(M.S.), ``Alias-free parameters in C using multibodies,'' Spring 2000--Summer 2001.

• 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] [PDF] [postscript]
• Medhat Assaad. Alias-free parameters in C using multibodies. Department of Computer Science, Iowa State University, TR #01-05, July 2001. [abstract] [PDF]
• Gzipped tar file with the sources for the C/ACL compiler

Arun D. Raghavan

(M.S.), ``Design of a JML documentation generator'', Fall 1999--summer 2000.

• Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Department of Computer Science, Iowa State University, TR #00-03e, March 2000, revised July, December 2000, August 2001, July 2003, May 2005. [abstract] [postscript] [PDF]

Abhay Bhorkar

(M.S.), ``A Run-time Assertion Checker for Java using JML,'' Spring 1998--Spring 2000.

• Abhay Bhorkar. A Run-time Assertion Checker for Java using JML. Department of Computer Science, Iowa State University, TR #00-08, May 2000. [abstract] [postscript].

Jianbing Chen

(M.S.), ``Dynamic Semantics and Type-checking of Tuple,'' Summer 1998--Fall 1998.

• Jianbing Chen. Dynamic Semantics and Type-checking of Tuple. Department of Computer Science, Iowa State University, TR #98-10, December 1998. [abstract] [postscript].

Anand Ganapathy

(M.S.), ``Design and Implementation of a JML Type Checker,'' Summer 1998--Spring 1999.

Olga Antropova

(M.S.), ``ACL Programming Language: Eliminating Parameter Aliasing with Dynamic Dispatch,'' September 1997--Summer 1998.

• 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]

Sevtap Otles Karakoy

(M.S.), ``Evaluating the Expressiveness of a Multi-Method Programming Language,'' September 1997--Summer 1998.

• Sevtap Otles Karakoy. Evaluating the Expressiveness of a Multi-Method Programming Language. Department of Computer Science, Iowa State University, TR #98-12, July, 1998. [abstract] [postscript].

Hua Zhong

(M.S.), ``LSL Traits for Using Z with Larch,'' January 1997--December 1997.

• Hua Zhong. LSL Traits for Using Z with Larch. Department of Computer Science, Iowa State University, TR #97-22, December, 1997. [abstract] [postscript].

Matthew W. Markland

(M.S.), ``Design and Implementation of the Larch/C++ Type System,'' Fall 1995--June 1998.

• Matthew W. Markland. Design and Implementation of the Larch/C++ Type System. Department of Computer Science, Iowa State University, TR #98-05, June, 1998. [abstract] [postscript].

Gowri Sankar Sivaprasad

(M.S.), ``Larch/CORBA: Specifying the Behavior of CORBA-IDL interfaces,'' Fall 1993--Fall 1995.

• Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of CORBA-IDL interfaces. Department of Computer Science, Iowa State University, TR #95-27, November, 1995. [abstract] [postscript].

Steven Jenkins

(M.S.), ``Polymorphic Type Checking in Scheme,'' Summer 1993--Spring 1995.

• Steven Jenkins and Gary T. Leavens. Polymorphic Type-Checking in Scheme. Computer Languages, 22(4): 215-223, 1996.

David Egle

(M.S.), ``Evaluating Larch/C++ as a Specification Language: A Case Study Using the Microsoft Foundation Class Library,'' Fall 1994--Summer 1995.

• David Egle. Evaluating Larch/C++ as a Specification Language: A Case Study Using the Microsoft Foundation Class Library. Department of Computer Science, Iowa State University, TR #95-17, July, 1995. [abstract] [postscript].

Joseph Reynolds

(M.S.), ``A Literate Executable, Denotational Semantics of Simple C++ Declarations,'' Fall 1991--Spring 1993.

• Joseph Reynolds. A Literate Executable, Denotational Semantics of Simple C++ Declarations. Department of Computer Science, Iowa State University, TR #93-15, 1993. [PDF].

Kari Lyle

(M.S.), ``Refinement in Data Flow Diagrams,'' Fall 1991--July 1992.

• 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] [postscript]

Yoonsik Cheon

(M.S.), ``Larch/Smalltalk: A Specification Language for Smalltalk,'' Fall 1990--Summer 1991.

• Yoonsik Cheon. Larch/Smalltalk: A Specification Language for Smalltalk. Department of Computer Science, Iowa State University, TR #91-15, 1991. [postscript].

Krishna Kishore Dhara

(Ph.D.), ``Behavioral Subtyping in Object-Oriented Programming Languages,'' Fall 1992--May 1997.

• 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 (editors), Foundations of Component-Based Systems, Cambridge University Press, 2000. Chapter 6, pages 113-135. [PDF], [postscript]
• Krishna Kishore Dhara. Behavioral Subtyping in Object-Oriented Languages. Department of Computer Science, Iowa State University, TR #97-09, May 1997. [abstract] [postscript] [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] [postscript] [PDF]
• 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.
• 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] [postscript]

Krishna Kishore Dhara

(M.S.), ``Subtyping Among Mutable Types in Object-Oriented Programming Languages,'' Spring 1990--Fall 1992

• Gary T. Leavens and Krishna Kishore Dhara. A Foundation for the Model Theory of Abstract Data Types with Mutation and Aliasing (preliminary version). Department of Computer Science, Iowa State University, TR #92-35, Novemember 1992. [postscript]

Timothy Wahls

(Ph.D.), ``On the Execution of High Level Formal Specifications,'' (joint with Professor Al Baker), Fall 1992--Spring 1995.

• Tim Wahls and Gary T. Leavens. Formal Semantics of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs. Proceedings of the 16th ACM Symposium on Applied Computing, Las Vegas, Nevada USA, March 11-14, 2001, pp. 567-575.
• 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]
• 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, 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] [postscript]
• Gary T. Leavens, Tim Wahls, and Albert L. Baker. Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages. In ACM SAC'99 -- 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] [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] [postscript]

Timothy Wahls

(M.S.), ``A Formal (and Executable) Semantics for RT-SPECS,'' (joint with Professor Al Baker), Fall 1991--Summer 1992.

Patricia O'Donnell

(M.S.), ``Implementation of the Programming Language Prosper,'' Fall 1989--Fall 1990.

Former Undergraduate (REU and 491) Students

Denise Bacher

REU working on JML specifications, Fall 2005

Jeff Beach

undergraduate honors research project, Spring 1990.

Katie Becker

Worked on JML specifications, espcially for java.util and java.io

Kristina P. Boysen

Worked on JML and in particular on graphical user interfaces for JML tools.

• 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]

Curtis Clifton

Worked on a type checker for Scheme.

David Faden

Worked on a type checker for Scheme.

Tabitha Johnson

REU working on JML specifications, Fall 2005 and Spring 2006

.

Grace Qiu

REU working on JML specifications, Fall 2005

Brandon Shilling

Worked on JML specifications, especially for java.lang's numeric types.

Elizabeth Seagren

Worked on JML specifications, especially for java.util.

Arthur Thomas

Worked on JML specifications, especially samples

Ajani Thomas

Worked on JML specifications, especially in java.util.

Elizabeth Weiss

Worked on a document explaining JML tools to new users.

Last update $Date: 2006/08/01 19:42:03 $