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.

Former Graduate Students at Foreign Universities

Henrique Rebêlo
(Ph.D.), Summer 2009--Spring 2014 (joint with Prof. Ricardo Massa Lima) at University of Pernambuco, Recife, Brazil.
  • Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman, Márcio Cornélio, and Thomas Thüm. AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts. To appear in Modularity 2014.
    [abstract] [Preprint PDF]
  • Henrique Rebêlo, Ricardo Lima, Gary T. Leavens, Márcio Cornélio, Alexandre Mota, and César Oliveria. Optimizing Generated Aspect-Oriented Assertion Checking Code for JML Using Program Transformations: An Empirical Study. Science of Computer Programming, 78(8):1137-1156, Aug. 2013. http://dx.doi.org/10.1016/j.scico.2012.09.003
  • Henrique Rebêlo, Gary T. Leavens, Ricardo Massa Ferreira Lima, Paulo Borba, and Márcio Ribeiro. Modular aspect-oriented design rule enforcement with XPIDRs. In FOAL '13 Proceedings of the 12th workshop on Foundations of aspect-oriented languages, 2013, pp. 13-18.
  • Henrique Rebêlo, Gary T. Leavens, and Ricardo Lima. Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-12-03, January 2012. [abstract] [Preprint PDF]
  • Henrique Rebêlo. Towards Client-Aware Interface Specifications. In Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion (SPLASH '11), Portland, Oregon, USA, October 22-27, 2011. [PDF].
  • Henrique Rebêlo, Ricardo Lima, and Gary T. Leavens. Modular Contracts with Procedures, Annotations, Pointcuts and Advice. To appear in the proceedings of the XV Brazilian Symposium on Programming Languages (SBLP 2011), Sao-Paulo, Brazil, September 29-30, 2011.
    Also Technical report CS-TR-11-05, Dept. of Electrical Engineering and Computer Science, University of Central Florida, September 2011. [abstract] [PDF]
  • Henrique Rebêlo, Roberta Coelho, Ricardo Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota, and Fernando Castor. On the Interplay of Exception Handling and Design by Contract: An Aspect-Oriented Recovery Approach. In FTFJP'11: Proceedings of the 13th Workshop on Formal Techniues for Java-Like Programs, article 7, 2011. http://dx.doi.org/10.1145/2076674.2076681
    Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-11-02, April 2011. [Abstract] [Preprint PDF]
  • Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, Gary T. Leavens, Alexandre Mota, and César Oliveira. Optimizing JML Feature Compilation in Ajmlc Using Aspect-Oriented Refactorings. In the proceedings of the XIII Brazilian Symposium on Programming Languages (SBLP 2009), Gramado-RS, Brazil, August 19-21, 2009.
    Also Technical report CS-TR-09-05, School of Electrical Engineering and Computer Science, University of Central Florida, April 2009. [abstract] [PDF]

Former Undergraduate (REU, etc.) Students at UCF

Nikole Solano
Gabrielle Mejia
Sean Merkel
Fred Gravil
Miguel Lopez
Silvino Barrieros
John Singleton
Fall 2012--Summer 2014.

Former Graduate Students and Finished Theses at UCF

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

Parisa Darbari Kozekanan
``Quantum Graph Parameters,'' Summer 2021--Summer 2022 (taking over from Dr. Pawel Wocjan)
Amirfarhad Nilizadeh
(Ph.D.), ``Test Overfitting in Automated Program Repair: Measurements and Approaches Using Formal Methods,'' Fall 2016--Summer 2022.
Kohei Koja
(M.S.), ``Translations to support loop invariant generation in JML,'' Spring 2021--Summer 2022.
Toby Tobkin
(Ph.D.), Fall 2013--summer 2016, quit didn't finish.
John Singleton
(Ph.D.), Fall 2014--Spring 2018.
Yuyan Bao
(Ph.D.), Fall 2010--Fall 2017.
  • 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
  • Yuyan Bao Reasoning About Frame Properties in Object-Oriented Programs. Computer Science, University of Central Florida, CS-TR-17-05, December 2017. [abstract] [Dissertation PDF]
  • Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Conditional Effects in Fine-grained Region Logic. Computer Science, University of Central Florida, CS-TR-15-01, March 2015. [abstract] [Preprint PDF]
  • Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Translating Separation Logic into Dynamic Frames Using Fine-Grained Region Logic. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-13-02a, March 2014. [abstract] [Preprint PDF]
Tushar Deshpande
(M.S.), Summer 2015-Summer 2016. TryOpenJML---A Verily based web application for learning about the Java Modeling Language, Summer, 2016. [PDF]
Arjun Mitra Reddy Donthala
(M.S.), Spring 2015--Summer 2016. Design of a Jmldoclet for jmldoc in OpenJML, Summer 2016. [PDF]
Faraz Hussain
(Ph.D.), Summer 2008--Spring 2016 (joint with Prof. Sumit Jha).
  • Faraz Hussain and Gary T. Leavens. temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties. In SEFM 2010: Proceedings of the 8th International Conference on Software Engineering and Formal Methods, Pisa, Italy, September 2010, pages 63-72, IEEE. http://dx.doi.org/10.1109/SEFM.2010.15
  • Ghaith Haddad, Faraz Hussain, and Gary T. Leavens. The Design of SafeJML, a Specification Language for SCJ with Support for WCET Specification. In JTRES '10: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, Prague, August 2010, pages 155-163. [PDF]
    Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-10-06, June 2010. [Preprint PDF]
José Sánchez
(Ph.D.), Fall 2011--Spring 2015.
Rochelle Elva
(Ph.D.), Fall 2008--Summer 2013 (formerly joint with Prof. David Workman).
  • Rochelle Elva. Detecting Semantic Method Clones in Java Code Using Method IOE-behavior. Computer Science, University of Central Florida, CS-TR-13-08, July 5, 2013. [abstract] [Dissertation PDF]
  • Rochelle Elva and Gary T. Leavens. JSCTracker: A Tool and Algorithm for Semantic Method Clone Detection Using Method IOE-Behavior. Computer Science, University of Central Florida, CS-TR-12-07, October 2012. [abstract] [PDF]
  • Rochelle Elva and Gary T. Leavens. Semantic Clone Detection using method IOE-behavior. 6th International Workshop on Software Clones (IWSC), Zurich, Switzerland, June 4, 2012, pages 80-81. http://dx.doi.org/10.1109/IWSC.2012.6227874.
  • Rochelle Elva and Gary T. Leavens. JSCTracker: A Semantic Clone Detection Tool for Java Code. Dept. of Computer Science, University of Central Florida, CS-TR-12-04, March 2012. [abstract] [PDF]
Alexandre Bassel
Fall 2009--Summer 2013 (joint with Prof. Fernando Gomez).
Cheng Wei
(M.S.), Fall 2011--Spring 2013.
Ghaith Haddad
(Ph.D.), Fall 2007--Fall 2012.

Former Graduate Students and Finished Theses at ISU

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

Steven Jenkins
(Ph.D.), Summer 1995--2007.
Steve M. Shaner
(M.S.), `` Modular verification of higher-order methods with mandatory calls specified by model programs,'' Spring 2005--Fall 2008.
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]
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. [Thesis PDF]
    Also Department of Computer Science, Iowa State University, TR #09-18, April 2009 [abstract] [TR 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
Dept. of Computer Science, University of Central Florida
329 L3Harris Center (Building 116)
Orlando, Florida 32816-2362 USA

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

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