Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Students of Gary T. Leavens
[go: Go Back, main page]

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 at UCF

Rochelle Elva
(Ph.D.), Fall 2008--present, joint with Prof. David Workman.
Faraz Hussain
(Ph.D.), Summer 2008--present. Fall 2006--April 2009.
Ghaith Haddad
(Ph.D.), Fall 2007--present.
  • Ghaith Haddad and Gary T. Leavens. Extensible Dynamic Analysis for JML: A Case Study with Loop Annotations. School of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-08-05, April 2008. [Preprint PDF]

Current Graduate Students at ISU

Steve M. Shaner
(Ph.D.), Summer 2007--present.
Neeraj Khanolkar
(M.S.), Summer 2005--May 2009, 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]
Steven Jenkins
(Ph.D.), Summer 1995--present.
Steve M. Shaner
(M.S.), `` Modular verification of higher-order methods with mandatory calls specified by model programs,'' Spring 2005--Fall 2008.

Current Undergraduate (REU, etc.) Students at UCF

Miguel Lopez and Silvino Barrieros.

Former Graduate Students and Finished Theses at ISU

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

Faraz Hussain
(M.S.), ``Enhancing a behavioral interface specification language with temporal logic features,'' Fall 2006--April 2009.
  • Faraz Hussain. Enhancing a behavioral interface specification language with temporal logic features. Department of Computer Science, Iowa State University, TR #09-18, April 2009. [abstract] [PDF]
Kristina Boysen Taylor
(M.S.), ``A Specification Language Design for the Java Modeling Language (JML) Using Java 5 Annotations,'' Summer 2005--Spring 2008.
  • Kristina B. Taylor, Johannes Rieken, and Gary T. Leavens. Adapting the Java Modeling Language for Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-06, April 2008. [abstract] [PDF]
  • Kristina B. Taylor. A Specification Language Design for the Java Modeling Language (JML) Using Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-03, April 2008. [abstract] [PDF]
  • Kristina P. Boysen and Gary T. Leavens. Discussion of Design Alternatives for JML Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-01, January 2008. [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]
Robert (Bob) Lavey
(M.S.), ``Tanager: A case study of iterative development in object-oriented analysis and design,'' Spring 1994--April 2007.
Clyde Ruby
(Ph.D.), ``Modular subclass verification: safely creating correct subclasses without superclass code,'' Spring 1995--Fall 2006.
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.
Brian J. Dorn
(M.S.), ``Design and implementation of a reusable type inference engine and its application to Scheme,'' Spring 2004--May 2005.
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.
  • Yoonsik Cheon, Antonio Cortes, Martine Ceberio, and Gary T. Leavens. Integrating Random Testing with Constraints for Improved Efficiency and Diversity. Department of Computer Science, The University of Texas at El Paso. TR \#08-07, May 2008. [PDF]
  • 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.
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.
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 at ISU

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 (now Kristina B. Taylor)
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.

Contact Information

Gary T. Leavens
School of Electrical Engineering and Computer Science, University of Central Florida
School of EECS, 439C Harris Center (Building 116)
Orlando, Florida 32816-2362 USA

e-mail: leavens@eecs.ucf.edu
Phone: +1-407-823-4758 / fax: +1-515-294-0258

Last update $Date: 2009/06/25 21:57:43 $