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
% $Id: leavens.bib,v 1.103 2006/05/19 19:20:50 leavens Exp $ % Bibliography for papers (co-)authored by Gary T. Leavens. % This bibliography is in BibTeX format. % % Entries are in alphabetical order by author's family name. %%% ==================================================================== %%% BibTeX-file{ %%% author = "Gary T. Leavens", %%% date = "$Date: 2006/05/19 19:20:50 $", %%% filename = "leavens.bib", %%% url = "ftp://ftp.cs.iastate.edu/pub/leavens/leavens.bib", %%% www-home = "http://www.cs.iastate.edu/~leavens/homepage.html", %%% address = "Department of Computer Science, %%% Iowa State University, %%% Ames, Iowa 50011-1040 USA", %%% telephone = "+1 515 294-1580", %%% FAX = "+1 515 294-0258", %%% FTP-archive = "ftp://ftp.cs.iastate.edu/pub/leavens/", %%% email = "leavens at cs.iastate.edu", %%% dates = {1980--}, %%% keywords = "type, specification, verification, object-oriented", %%% supported = "yes", %%% supported-by = "Gary T. Leavens ", %%% abstract = "Bibliography for Gary T. Leavens" %%% } %%% ==================================================================== @string{ACM = "ACM"} @string{LNCS = "Lecture Notes in Computer Science"} @string{MITLCS = "Massachusetts Institute of Technology, Laboratory for Computer Science"} @string{NY = "New York, NY"} @string{POPL = "Annual ACM Symposium on Principles of Programming Languages"} @string{SIGPLAN = "ACM SIGPLAN Notices"} % TOPLAS="ACM Transactions on Programming Languages and Systems" @TechReport{Assaad-Leavens01, key = {Assaad \& Leavens}, author = {Medhat G. Assaad and Gary T. Leavens}, title = {Alias-free parameters in {C} for Better Reasoning and Optimization}, institution = "Department of Computer Science, Iowa State University", year = 2001, number = "01-11", address = "226 Atanasoff Hall, Ames, Iowa 50011", month = Nov, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR01-11/TR.pdf", Note = "Available from archives.cs.iastate.edu.", Annote = "Applies the ACL approach to C. Describes the optimization opportunities that arise. 33 references." } @TechReport{Boysen-Leavens05, key = {Boysen \& Leavens}, author = {Kristina P. Boysen and Gary T. Leavens}, title = {Automatically generating consistent graphical user interfaces using a parser generator}, institution = "Department of Computer Science, Iowa State University", year = 2005, number = "04-07a", address = "226 Atanasoff Hall, Ames, Iowa 50011", month = Nov, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR04-07/TR.pdf", Note = "Available from archives.cs.iastate.edu.", Annote = "13 references." } @Article{Bruce-etal95, Key = "Bruce, {\em et al.}", Author = "Kim Bruce and Luca Cardelli and Giuseppe Castagna and The Hopkins Object Group and Gary T. Leavens and Benjamin Pierce", Title = "On Binary Methods", Journal = "Theory and Practice of Object Systems", Publisher = "John, Wiley and Sons, Inc.", Year = 1995, Address = NY, Pages = "221-242", Volume = 1, Number = 3, Annote = "53 references." } @TechReport{Bruce-etal95a, Key = "Bruce, {\em et al.}", Author = "Kim Bruce and Luca Cardelli and Giuseppe Castagna and The Hopkins Object Group and Gary T. Leavens and Benjamin Pierce", Title = "On Binary Methods", Year = 1995, Month = Dec, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "95-08a", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR95-08/TR.ps.Z", Note = "Appears in {\it Theory and Practice of Object Systems}. Volume 1, Number 3. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu" } @InProceedings{Burdy-etal03, key = {Burdy, {\it et al.}}, author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joeseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll}, title = {An overview of {JML} tools and applications}, booktitle = {Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03)}, pages = {73--89}, year = {2003}, editor = {Thomas Arts and Wan Fokkink}, volume = {80}, series = {Electronic Notes in Theoretical Computer Science (ENTCS)}, month = {June}, publisher = {Elsevier}, annote = {42 references.}, URL = {http://www.sciencedirect.com/science/journal/15710661} } @TechReport{Burdy-etal03a, key = {Burdy, {\it et al.}}, author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joeseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll}, title = {An overview of {JML} tools and applications}, institution = {Dept. of Computer Science, University of Nijmegen}, year = {2003}, number = {NIII-R0309}, annote = {42 references.}, URL = {ftp://ftp.cs.iastate.edu/pub/leavens/JML/jml-white-paper.pdf} } @Article{Burdy-etal05, key = {Burdy, {\it et al.}}, author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joeseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll}, title = {An overview of {JML} tools and applications}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = 7, number = 3, month = Jun, year = {2005}, publisher = {Springer-Verlag}, pages = {212--232}, annotate = {93 references.} } @Article{Castagna-Leavens95, key = "Castagna \& Leavens", author = "Giuseppe Castagna and Gary T. Leavens", title = "Foundations of Object-Oriented Languages (2nd Workshop report)", journal = SIGPLAN, year = 1995, volume = 30, number = 2, pages = "5-11", month = Feb, annote = "21 references." } @InProceedings{Chambers-Leavens94, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "Typechecking and Modules for Multi-Methods", BookTitle = "OOPSLA '94 Conference Proceedings", Series = SIGPLAN, Volume = "29(10)", Month = Oct, Year = 1994, Pages = "1-15", Annote = "Over 47 references." } @TechReport{Chambers-Leavens94b, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "Towards Safe Modular Extensible Objects", Institution = "Department of Computer Science, Iowa State University", Year = 1994, Number = "94-17a", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Sep, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-17/TR.ps.Z", Note = "Appears in {\it OOPSLA '94 Workshop Proceedings: Subjectivity in Object-Oriented Systems}" } @TechReport{Chambers-Leavens94c, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "Typechecking and Modules for Multi-Methods", Institution = "Department of Computer Science, Iowa State University", Year = 1994, Number = "94-03a", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-03/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu. Also University of Washington Department of Computer Science and Engineering TR number 94-03-01. A shorter version appears in the {\em OOPSLA '94 Conference Proceedings}, pages 1--15.", Annote = "Over 47 references." } @TechReport{Chambers-Leavens95, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "Typechecking and Modules for Multi-Methods", Institution = "Department of Computer Science, Iowa State University", Year = 1995, Number = "95-19", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR95-19/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu. Also University of Washington Department of Computer Science and Engineering TR number 95-08-05. Appears in {\em ACM TOPLAS}, vol 17, num 6, pages 805-843.", Annote = "Over 47 references." } @Article{Chambers-Leavens95b, author = "Craig Chambers and Gary T. Leavens", title = "Typechecking and Modules for Multi-Methods", key = "Chambers \& Leavens", journal = "TOPLAS", year = 1995, volume = 17, number = 6, pages = "805-843", month = Nov, annote = "56 references." } @InProceedings{Chambers-Leavens96, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "{BeCecil}, A Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing", booktitle = {The Fourth International Workshop on Foundations of Object-Oriented Languages, {FOOL 4}, Paris, France}, Year = 1996, Month = Dec, note = {The proceedings are on-line at the URL http://www.cs.williams.edu/\verb|~|kim/FOOL/FOOL4.html}, annote = {Many references.}, URL = "http://www.cs.indiana.edu/hyplan/pierce/fool/chambers.ps.gz" } @TechReport{Chambers-Leavens97, Key = "Chambers \& Leavens", Author = "Craig Chambers and Gary T. Leavens", Title = "{BeCecil}, A Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing", Institution = "Department of Computer Science, Iowa State University", Year = 1997, Number = "96-17a", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-17/TR.ps.gz", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu. Also University of Washington Department of Computer Science and Engineering TR number UW-CSE-96-12-02.", Annote = "Many references." } @TechReport{Cheon-Hayashi-Leavens03, Key = "Cheon \& Hayashi \& Leavens", Author = "Yoonsik Cheon and Yoshiki Hayashi and Gary T. Leavens", Title = "A Thought on Specification Reflection", Institution = "Department of Computer Science, Iowa State University", Month = Dec, Year = 2003, Number = "03-16", Note = "Available from \url{archives.cs.iastate.edu}. To appear in (SCI 2004).", Annote = "21 references." } @TechReport{Cheon-Leavens01, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Simple and Practical Approach to Unit Testing: The {JML} and {JUnit} Way", Institution = "Department of Computer Science, Iowa State University", Month = Nov, Year = 2001, Number = "01-12", Note = "Available from archives.cs.iastate.edu.", Annote = "51 references." } @InProceedings{Cheon-Leavens02, key = {Cheon \& Leavens}, author = {Yoonsik Cheon and Gary T. Leavens}, title = {A Simple and Practical Approach to Unit Testing: The {JML} and {JUnit} Way}, booktitle = {ECOOP 2002 --- Object-Oriented Programming, 16th European Conference, M\'{a}alaga, Spain, Proceedings}, pages = {231-255}, year = 2002, editor = {Boris Magnusson}, volume = 2374, series = LNCS, address = {Berlin}, month = Jun, publisher = {Springer-Verlag}, annote = {The jmlunit tool. 38 references.} } @TechReport{Cheon-Leavens02a, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Simple and Practical Approach to Unit Testing: The {JML} and {JUnit} Way", Institution = "Department of Computer Science, Iowa State University", Month = Mar, Year = 2002, Number = "01-12a", Note = "Appears in ECOOP 2002 proceedings, LNCS 2374, pp. 231-255.", Annote = "51 references." } @InProceedings{Cheon-Leavens02b, key = {Cheon \& Leavens}, author = {Yoonsik Cheon and Gary T. Leavens}, title = {A Runtime Assertion Checker for the {Java Modeling Language (JML)}}, booktitle = {Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, USA, June 24-27, 2002}, pages = {322--328}, year = 2002, editor = {Hamid R. Arabnia and Youngsong Mun}, month = Jun, publisher = {CSREA Press}, annote = {23 references.}, url = {ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf} } @TechReport{Cheon-Leavens02c, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Runtime Assertion Checker for the {Java Modeling Language (JML)}", Institution = "Department of Computer Science, Iowa State University", Month = Mar, Year = 2002, Number = "02-05", Note = "In SERP 2002, pp. 322-328", Annote = "19 references.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf" } @TechReport{Cheon-Leavens04, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "The {JML} and {JUnit} Way of Unit Testing and its Implementation", Institution = "Department of Computer Science, Iowa State University", Month = Apr, Year = 2004, Number = "04-02a", Annote = "51 references.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR04-02/TR.pdf" } @InProceedings{Cheon-Leavens05, key = {Cheon \& Leavens}, author = {Yoonsik Cheon and Gary T. Leavens}, title = {A Contextual Interpretation of Undefinedness for Runtime Assertion Checking}, booktitle = {AADEBUG 2005, Proceedings of the Sixth International Symposium on Automated and Analysis-Driven Debugging, Monterey, California, September 19--21, 2005}, pages = {149--157}, year = 2005, month = Sep, publisher = {ACM Press}, annote = {30 references.} } @TechReport{Cheon-Leavens05a, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Contextual Interpretation of Undefinedness for Runtime Assertion Checking", Institution = "Department of Computer Science, The University of Texas at El Paso", Month = Mar, Year = 2005, Number = "05-10", Note = "Submitted for publication", Annote = "28 references.", URL = "http://www.cs.utep.edu/~cheon/techreport/tr05-10.pdf" } @TechReport{Cheon-Leavens93a, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Quick Overview of {Larch/C++}", Institution = "Department of Computer Science, Iowa State University", Month = Jun, Year = 1994, Number = "93-18a", Note = "Appears in the {\em Journal of Object-Oriented Programming\/}, 7(6):39-49, October 1994.", Annote = "29 references." } @Article{Cheon-Leavens94, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "The {Larch/Smalltalk} Interface Specification Language", Journal = "ACM Transactions on Software Engineering and Methodology", Month = Jul, Year = 1994, Volume = 3, Number = 3, Pages = "221-253", Annote = "44 references." } @TechReport{Cheon-Leavens94b, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "The {Larch/Smalltalk} Interface Specification Language", Institution = "Department of Computer Science, Iowa State University", Month = May, Year = 1994, Number = "93-24a", Note = "Appeared in {\it ACM TOSEM}, July 1994, pages 221-253. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu.", Annote = "44 references." } @TechReport{Cheon-Leavens94c, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A gentle introduction to {Larch/Smalltalk} specification browsers", Institution = "Department of Computer Science, Iowa State University", Month = Jan, Year = 1994, Number = "94-01", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-01/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu." } @Article{Cheon-Leavens94d, Key = "Cheon \& Leavens", Author = "Yoonsik Cheon and Gary T. Leavens", Title = "A Quick Overview of {Larch/C++}", Journal = "Journal of Object-Oriented Programming", Year = 1994, Volume = 7, Number = 6, Month = Oct, Pages = "39-49", Annote = "29 references." } @TechReport{Cheon-etal03, Key = "Cheon \& Leavens \& Sitaraman \& Edwards", Author = "Yoonsik Cheon and Gary T. Leavens and Murali Sitaraman and Stephen Edwards", Title = "Model Variables: Cleanly Supporting Abstraction in Design By Contract", Institution = "Department of Computer Science, Iowa State University", Month = Sep, Year = 2003, Number = "03-10a", Note = "To appear in \emph{Software -- Practice \& Experience}. Available from \url{archives.cs.iastate.edu}.", Annote = "39 references." } @TechReport{Cheon-etal04, Key = "Cheon \& Leavens \& Sitaraman \& Edwards", Author = "Yoonsik Cheon and Gary T. Leavens and Murali Sitaraman and Stephen Edwards", Title = "Model Variables: Cleanly Supporting Abstraction in Design By Contract", Institution = "Department of Computer Science, Iowa State University", Month = Aug, Year = 2004, Number = "03-10b", Note = "To appear in \emph{Software -- Practice \& Experience}. Available from \url{archives.cs.iastate.edu}.", Annote = "26 references." } @Article{Cheon-etal05, Key = "Cheon \& Leavens \& Sitaraman \& Edwards", Author = "Yoonsik Cheon and Gary T. Leavens and Murali Sitaraman and Stephen Edwards", Title = "Model Variables: Cleanly Supporting Abstraction in Design By Contract", Journal = SPandE, Year = 2005, Volume = 35, Number = 6, Month = May, Pages = "583--599", Annote = "DOE: 10.1002/see.649" } @TechReport{Clifton-Leavens-Wand03, Key = {Clifton \& Leavens \& Wand}, Author = {Curtis Clifton and Gary T. Leavens and Mitchell Wand}, Title = {Formal Definition of the Parameterized Aspect Calculus}, institution = {Iowa State University, Department of Computer Science}, year = 2003, number = {03-12b}, month = Nov, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-12/TR.pdf" } @TechReport{Clifton-Leavens-Wand03a, Key = {Clifton \& Leavens \& Wand}, Author = {Curtis Clifton and Gary T. Leavens and Mitchell Wand}, Title = {Parameterized Aspect Calculus: A Core Calculus for the Direct Study of Aspect-Oriented Languages}, institution = {Iowa State University, Department of Computer Science}, year = 2003, number = {03-13}, month = Oct } @TechReport{Clifton-Leavens02, Key = {Clifton \& Leavens}, Author = {Curtis Clifton and Gary T. Leavens}, Title = {Observers and Assistants: A Proposal for Modular Aspect-Oriented Reasoning}, institution = {Iowa State University, Department of Computer Science}, year = 2002, number = {02-04a}, month = Apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-04/TR.pdf", Annote = "25 references." } @InProceedings{Clifton-Leavens02a, Key = {Clifton \& Leavens}, Author = {Curtis Clifton and Gary T. Leavens}, Title = {Observers and Assistants: A Proposal for Modular Aspect-Oriented Reasoning}, Pages = "33-44", BookTitle = {FOAL 2002 Proceedings: Foundations of Aspect-Oriented Languages Workshop at AOSD 2002}, year = 2002, Editor = {Gary T. Leavens and Ron Cytron}, Organization = {Department of Computer Science, Iowa State University}, Series = {Technical Report}, number = {02-06}, month = Apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-06/TR.pdf" } @TechReport{Clifton-Leavens02b, Key = {Clifton \& Leavens}, Author = {Curtis Clifton and Gary T. Leavens}, Title = {Spectators and Assistants: Enabling Modular Aspect-Oriented Reasoning}, institution = {Iowa State University, Department of Computer Science}, year = 2002, number = {02-10}, month = Oct, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-10/TR.pdf", Annote = "29 references." } @InProceedings{Clifton-Leavens03, Key = {Clifton \& Leavens}, Author = {Curtis Clifton and Gary T. Leavens}, Title = {Obliviousness, Modular Reasoning, and the Behavioral Subtyping Analogy}, institution = {Iowa State University, Department of Computer Science}, year = 2003, BookTitle = {SPLAT 2003: Software engineering Properties of Languages for Aspect Technologies at AOSD 2003}, month = Mar, note = "Available as Computer Science Technical Report TR03-01a from ftp//:ftp.cs.iastate.edu/pub/techreports/TR03-01/TR.pdf", Annote = "19 references." } @TechReport{Clifton-Leavens03a, Key = {Clifton \& Leavens}, Author = {Curtis Clifton and Gary T. Leavens}, Title = {Obliviousness, Modular Reasoning, and the Behavioral Subtyping Analogy}, institution = {Iowa State University, Department of Computer Science}, year = 2003, number = {03-15}, month = Dec, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-15/TR.pdf", Annote = "19 references.", Note = {Revised version of TR03-01} } @InProceedings{Clifton-Leavens05, author = {Curtis Clifton and Gary T. Leavens}, title = {MiniMAO: Investigating the Semantics of Proceed}, key = {Clifton \& Leavens}, booktitle = {FOAL 2005 Proceedings: Foundations of Aspect-Oriented Languages Workshop at AOSD 2005, Chicago, IL}, pages = {57-67}, year = 2005, editor = {Curtis Clifton and Ralf L\"{a}mmel and and Gary T. Leavens}, number = {05-05}, series = {TR}, address = {Ames, IA, 50011}, month = Mar, organization = {Dept. of Computer Science, Iowa State University}, URL = "\url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2005/proceedings.pdf}", annote = {18 references.} } @TechReport{Clifton-Leavens05a, key = {Clifton \& Leavens}, author = {Curtis Clifton and Gary T. Leavens}, title = {MiniMAO$_1$: Investigating the Semantics of Proceed}, year = 2005, number = {05-01}, address = {Ames, IA, 50011}, month = Jan, institution = {Dept. of Computer Science, Iowa State University}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR05-01/TR.pdf", annote = {17 references.} } @TechReport{Clifton-Leavens05b, key = {Clifton \& Leavens}, author = {Curtis Clifton and Gary T. Leavens}, title = {A Design Discipline and Language Features for Formal Modular Reasoning in Aspect-Oriented Programs}, year = 2005, number = {05-23}, address = {Ames, IA, 50011}, month = Jan, institution = {Dept. of Computer Science, Iowa State University}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR05-23/TR.pdf", annote = {35 references.} } @InProceedings{Clifton-etal00, Key = {Clifton, {\em et al.}}, Author = {Curtis Clifton and Gary T. Leavens and Craig Chambers and Todd Millstein}, Title = {{MultiJava}: Modular Open Classes and Symmetric Multiple Dispatch for {Java}}, BookTitle = "OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota", Series = SIGPLAN, Volume = "35(10)", Month = Oct, Year = 2000, Pages = "130-145", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-06/TR.ps.gz", Annote = "32 references." } @TechReport{Clifton-etal00a, author = {Curtis Clifton and Gary T. Leavens and Craig Chambers and Todd Millstein}, title = {{MultiJava}: Modular Open Classes and Symmetric Multiple Dispatch for {Java}}, institution = {Iowa State University, Department of Computer Science}, year = 2000, key = {Clifton, {\em et al.}}, number = {00-06a}, month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-06/TR.ps.gz", Note = "Appears in OOPSLA 2000 Conference Proceedings, pp. 130-145.", Annote = "32 references." } @TechReport{Clifton-etal04, key = {Clifton, {\em et al.}}, author = {Curtis Clifton and Todd Millstein and Gary T. Leavens and Craig Chambers}, title = {{MultiJava}: Design Rationale, Compiler Implementation, and Applications}, institution = {Iowa State University, Dept. of Computer Science}, year = {2004}, number = {04-01b}, month = Dec, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR04-01/TR.pdf", note = "Accepted for publication, pending revision", annote = {many references} } @Article{Clifton-etal05a, key = {Clifton, {\em et al.}}, author = {Curtis Clifton and Todd Millstein and Gary T. Leavens and Craig Chambers}, title = {{MultiJava}: Design Rationale, Compiler Implementation, and Applications}, journal = TOPLAS, note = {To appear, preliminary version available from \url{ftp://ftp.cs.iastate.edu/pub/techreports/TR04-01/TR.pdf} on July 17, 2005}, year = {2005}, annote = {80 references} } @TechReport{Dhara-Leavens01, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens ", Title = "Preventing Cross-Type Aliasing for More Practical Reasoning", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "01-02a", Year = 2001, Month = Nov, Note = "Available from archives.cs.iastate.edu", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.pdf", Annote = "54 references." } @TechReport{Dhara-Leavens92, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens ", Title = "Subtyping for mutable types in object-oriented programming languages", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "92-36", Year = 1992, Month = Nov, Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "21 references." } @TechReport{Dhara-Leavens94, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens", Title = "Weak Behavioral Subtyping for Types with Mutable Objects", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "94-21", Year = 1994, Month = Nov, Note = "Appears in Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, Preliminary Proceedings, pages 269-290. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "15 references." } @InProceedings{Dhara-Leavens95, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens ", title = "Weak Behavioral Subtyping for Types with Mutable Objects", editor = "S. Brookes and M. Main and A. Melton and M. Mislove", booktitle = "Mathematical Foundations of Programming Semantics, Eleventh Annual Conference", year = 1995, Series = "Electronic Notes in Theoretical Computer Science", publisher = "Elsevier", Volume = 1, note = "http://www.sciencedirect.com/science/journal/15710661", annote = "20 references." } @TechReport{Dhara-Leavens95b, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens", Title = "Forcing Behavioral Subtyping Through Specification Inheritance", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "95-20c", Year = 1997, Month = Dec, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz", Note = "Also in Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, 1996, pp. 258--267. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "21 references." } @InProceedings{Dhara-Leavens95c, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens ", title = "Weak Behavioral Subtyping for Types with Mutable Objects", editor = "S. Brookes and M. Main and A. Melton and M. Mislove", booktitle = "Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, Preliminary Proceedings", pages = "269-290", year = 1995, publisher = "Elsevier", month = "March", note = "The final version is in {\it Electronic Notes in Theoretical Computer Science}, volume 1, which is on-line at http://www.sciencedirect.com/science/journal/15710661", annote = "20 references." } @InProceedings{Dhara-Leavens96, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens", Title = "Forcing Behavioral Subtyping Through Specification Inheritance", BookTitle = "Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany", Publisher = "IEEE Computer Society Press", Pages = "258-267", Year = 1996, Month = Mar, Note = "A corrected version is Iowa State University, Dept. of Computer Science TR \#95-20c.", Annote = "19 references." } @InProceedings{Drossopoulou-etal00, author = {Sophia Drossopoulou and Susan Eisenbach and Bart Jacobs and Gary T. Leavens and Peter M{\"u}ller and Arnd Poetzsch-Heffter}, title = {Formal Techniques for {J}ava Programs}, booktitle = {Object-Oriented Technology. {ECOOP} 2000 Workshop Reader}, year = 2000, editor = {Jacques Malenfant and Sabine Moisan and Ana Moreira}, series = LNCS, volume = 1964, publisher = {Springer-Verlag}, pages = {41-54} } @Proceedings{Drossopoulou-etal00b, key = {Drossopoulou, {\em et al.}}, editor = {Sophia Drossopoulou and Susan Eisenbach and Bart Jacobs and Gary T. Leavens and Peter M{\"u}ller and Arnd Poetzsch-Heffter}, title = {Formal Techniques for {Java} Programs}, year = 2000, organization = {Technical Report~269, Fernuniversit{\"a}t Hagen}, note = {Available from \verb+www.informatik.fernuni-hagen.de/pi5/publications.html+.} } @InProceedings{Drossopoulou-etal02, author = {Sophia Drossopoulou and Susan Eisenbach and Gary T. Leavens and Arnd Poetzsch-Heffter and Erik Poll}, title = {Formal Techniques for {J}ava-like Programs}, booktitle = {Object-Oriented Technology. {ECOOP} 2002 Workshop Reader}, year = 2002, editor = {Juan Hernandez and Ana Moreira}, series = LNCS, volume = 2548, publisher = {Springer-Verlag}, pages = {203-210}, annote = "4 references." } @Article{Eisenbach-Leavens01, author = {Susan Eisenbach and Gary T. Leavens}, title = {Special Issue: formal techniques for {Java} programs}, journal = {Concurrency and Computation: Practice and Experience}, year = 2001, key = {Eisenbach \& Leavens}, volume = 13, number = 3 } @Proceedings{FOAL02, Key = "FOAL", Editor = "Gary T. Leavens and Ron Cytron", Title = "{FOAL} 2002 Proceedings: Foundations of Aspect-Oriented Langauges Workshop at {AOSD} 2002", Year = 2002, Month = Apr, Address = "Enschede, The Netherlands", URL = "http://www.cs.iastate.edu/~leavens/FOAL/papers-2002/TR.pdf", Note = "Available as Technical Report 02-06, Department of Computer Science, Iowa State University. \url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2002/TR.pdf}" } @Proceedings{FOAL03, Key = "FOAL", Editor = "Gary T. Leavens and Curtis Clifton", Title = "{FOAL} 2003 Proceedings: Foundations of Aspect-Oriented Langauges Workshop at {AOSD} 2003", Year = 2003, Month = Mar, Address = "Boston, MA", URL = "http://www.cs.iastate.edu/~leavens/FOAL/papers-2003/proceedings.pdf", Note = "Available as Technical Report 03-05, Department of Computer Science, Iowa State University. \url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2003/proceedings.pdf}" } @Proceedings{FOAL04, Key = "FOAL", Editor = {Curtis Clifton and Ralf L\"{a}mmel and Gary T. Leavens}, Title = "{FOAL} 2004 Proceedings: Foundations of Aspect-Oriented Langauges Workshop at {AOSD} 2004", Year = 2004, Month = Mar, Address = "Lancaster, UK", URL = "http://www.cs.iastate.edu/~leavens/FOAL/papers-2004/proceedings.pdf", Note = "Available as Technical Report 04-04, Department of Computer Science, Iowa State University. \url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2004/proceedings.pdf}" } @Proceedings{FOAL05, key = {Clifton \& L\"{a}mmel \& Leavens}, editor = {Curtis Clifton and Ralf L\"{a}mmel and and Gary T. Leavens}, title = {{FOAL} 2005 Proceedings: Foundations of Aspect-Oriented Languages Workshop at {AOSD} 2005}, year = 2005, address = {Chicago, IL}, month = Mar, URL = "\url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2005/proceedings.pdf}", Note = "Available as Technical Report 05-05, Department of Computer Science, Iowa State University. \url{http://www.cs.iastate.edu/~leavens/FOAL/papers-2005/proceedings.pdf}" } @InProceedings{Jacobs-etal99, author = {B. Jacobs and G. T. Leavens and P. M{\"u}ller and A. Poetzsch-Heffter}, title = {Formal Techniques for {Java} Programs}, booktitle = {Object-Oriented Technology. {ECOOP}'99 Workshop Reader}, year = 1999, editor = {A. Moreira and D. Demeyer}, series = LNCS, volume = 1743, publisher = {Springer-Verlag}, note = {Available from \verb+www.informatik.fernuni-hagen.de/pi5/publications.html+}, URL = {http://www.informatik.fernuni-hagen.de/pi5/publications.html} } @Article{Jenkins-Leavens96, Key = "Jenkins \& Leavens", Author = "Steven Jenkins and Gary T. Leavens ", Title = "Polymorphic Type-Checking in Scheme", Journal = "Computer Lanugages", Volume = 22, Number = 4, Year = 1996, Pages = "215-223", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR95-21/TR.ps.Z", Annote = "13 references." } @TechReport{Kulczycki-etal02, Key = {Kulczycki, {\it et al.}}, Author = {Gregory W. Kulczycki and Murali Sitaraman and William F. Ogden and Bruce W. Weide and Gary T. Leavens}, Title = "Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "02-13", Year = 2002, Month = Dec, Annote = "Call by swapping compared with other mechanisms. 50 references." } @TechReport{Kulczycki-etal03, Key = {Kulczycki, {\it et al.}}, Author = {Gregory W. Kulczycki and Murali Sitaraman and William F. Ogden and Gary T. Leavens}, Title = "Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "02-13a", Year = 2003, Month = Dec, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-13/TR.pdf", Annote = "Three approaches to avoiding aliasing due to repeated arguments. 63 references." } @TechReport{Leavens-Antropova99, Key = "Leavens \& Antropova", Author = "Gary T. Leavens and Olga Antropova", Title = "{ACL} --- Eliminating Parameter Aliasing with Dynamic Dispatch", Year = 1999, Month = Feb, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "98-08a", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-08/TR.ps.gz", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu" } @TechReport{Leavens-Baker-Ruby06, Key = "Leavens \& Baker \& Ruby", Author = "Gary T. Leavens and Albert L. Baker and Clyde Ruby", Title = "Preliminary Design of {JML}: A Behavioral Interface Specification Language for {Java}", Institution = "Iowa State University, Department of Computer Science", Year = 2006, Number = "98-06-rev29", Month = Jan, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.pdf", Annote = "79 references.", Note = "To appear in \emph{ACM SIGSOFT Software Engineering Notes}." } @InProceedings{Leavens-Baker-Ruby98, author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby}, title = {{JML}: a {Java Modeling Language}}, booktitle = {Formal Underpinnings of Java Workshop (at OOPSLA '98)}, key = {Leavens \& Baker \& Ruby}, year = 1998, month = Oct, note = {{\tt http://www-dse.doc.ic.ac.uk/{\char'176}sue/oopsla/cfp.html}} } @InCollection{Leavens-Baker-Ruby99b, Key = "Leavens \& Baker \& Ruby", Author = "Gary T. Leavens and Albert L. Baker and Clyde Ruby", Title = "{JML}: A Notation for Detailed Design", BookTitle = "Behavioral Specifications of Businesses and Systems", Editor = "Haim Kilov and Bernhard Rumpe and Ian Simmonds", Year = 1999, Publisher = "Kluwer Academic Publishers", Address = "Boston", Pages = "175-188", Annote = "36 references." } @InProceedings{Leavens-Baker99, Key = "Leavens \& Baker", Author = "Gary T. Leavens and Albert L. Baker", Title = "Enhancing the Pre- and Postcondition Technique for More Expressive Specifications", Editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies", BookTitle = "FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings", Year = 1999, Series = LNCS, Publisher = "Springer-Verlag", Volume = 1709, Pages = "1087--1106", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-19/TR.ps.gz", Annote = "37 references." } @TechReport{Leavens-Baker99a, Key = "Leavens \& Baker", Author = "Gary T. Leavens and Albert L. Baker", Title = "Enhancing the Pre- and Postcondition Technique for More Expressive Specifications", Institution = "Iowa State University, Department of Computer Science", Year = 1999, Number = "97-19b", Month = Jun, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-19/TR.ps.gz", Annote = "37 references.", Note = "Appears in FM'99, Springer-Verlag, LNCS volume 1709, pages 1087--1106, 1999." } @TechReport{Leavens-Cheon-Cok05, Key = "Leavens \& Cheon \& Cok", Author = "Gary T. Leavens and Yoonsik Cheon and David R. Cok", Title = "Demonstration of {JML} Tools", Institution = "Iowa State University, Department of Computer Science", Address = "226 Atanasoff Hall, Ames IA 50011", Year = 2005, Number = "05-13", Month = Apr, Note = "Available by anonymous ftp from ftp.cs.iastate.edu.", URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-13/TR.pdf}, Annote = "14 references." } @Unpublished{Leavens-Cheon05, Key = "Leavens \& Cheon", Author = "Gary T. Leavens and Yoonsik Cheon", Title = "Design by Contract with JML", Year = 2005, Note = "Draft, available from jmlspecs.org.", URL = "ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdf", Annote = "12 references." } @TechReport{Leavens-Cheon92a, Key = "Leavens \& Cheon", Author = "Gary T. Leavens and Yoonsik Cheon", Title = "Preliminary Design of {Larch/C++}", Institution = "Iowa State University, Department of Computer Science", Address = "226 Atanasoff Hall, Ames IA 50011", Year = 1992, Number = "92-16", Month = May, Note = "Presented at the First International Workshop on Larch, Dedham, Mass., July, 1992.", Annote = "26 references." } @InCollection{Leavens-Cheon92b, Key = "Leavens \& Cheon", Author = "Gary T. Leavens and Yoonsik Cheon", Title = "Preliminary Design of {Larch/C++}", BookTitle = "Proceedings of the First International Workshop on Larch, July, 1992", Publisher = "Springer-Verlag", Editor = "U. Martin and J. Wing", Series = "Workshops in Computing", Pages = "159-184", Address = NY, Year = 1993, Annote = "26 references." } @TechReport{Leavens-Cheon93b, Key = "Leavens \& Cheon", Author = "Gary T. Leavens and Yoonsik Cheon", Title = "Extending {CORBA IDL} to Specify Behavior with {Larch}", Institution = "Iowa State University, Department of Computer Science", Year = 1993, Number = "93-20", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-20/TR.txt", Note = "Presented at the OOPSLA '93 Workshop: ``Specification of Behavioral Semantics in OO Information Modeling''. Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "Discusses Larch/CORBA. 6 references." } @TechReport{Leavens-Cheon94d, Key = "Leavens \& Cheon", Author = "Gary T. Leavens and Yoonsik Cheon", Title = "Overview and Specification of the Built-in Types in {Little Smalltalk}", Institution = "Iowa State University, Department of Computer Science", Year = 1994, Number = "91-22a", Address = "226 Atanasoff Hall, Ames IA 50011", Month = Feb, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR91-22/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu." } @TechReport{Leavens-Clifton05, author = {Gary T. Leavens and Curtis Clifton}, title = {A Type Notation for {Scheme}}, key = {Leavens \& Clifton}, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "05-03", Year = 2005, Month = Feb, Note = "Available by anonymous ftp from ftp.cs.iastate.edu.", URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-03/TR.pdf}, Annote = "8 references." } @Proceedings{Leavens-Clifton05a, key = {Leavens \& Clifton}, title = {Lessons from the {JML} Project}, year = 2005, booktitle = {Verified Software: Theories, Tools, Experiments, Zurich, Switzerland}, month = {Oct}, organization = {IFIP Working Group 2.3}, note = {To appear. Also ISU TR \#05-12a, July 2005}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.pdf}, Annote = "30 references." } @TechReport{Leavens-Clifton05b, author = {Gary T. Leavens and Curtis Clifton}, title = {Lessons from the {JML} Project}, key = {Leavens \& Clifton}, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "05-12a", Year = 2005, Month = Jul, Note = "Available by anonymous ftp from ftp.cs.iastate.edu.", URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.pdf}, Annote = "30 references." } @TechReport{Leavens-Clifton-Dorn06, key = {Leavens \& Clifton \& Dorn}, author = {Gary T. Leavens and Curtis Clifton and Brian Dorn}, title = {A Type Notation for {Scheme}}, Year = 2006, Month = Jan, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "05-18a", Note = "Available by anonymous ftp from ftp.cs.iastate.edu.", URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-18/TR.pdf}, Annote = "7 references." } @InCollection{Leavens-Dhara00, key = {Leavens \& Dhara}, author = {Gary T. Leavens and Krishna Kishore Dhara}, title = {Concepts of Behavioral Subtyping and a Sketch of Their Extension to Component-Based Systems}, booktitle = {Foundations of Component-Based Systems}, publisher = {Cambridge University Press}, year = 2000, editor = {Gary T. Leavens and Murali Sitaraman}, chapter = 6, pages = {113-135}, URL = {http://www.cs.iastate.edu/~leavens/FoCBS-book/06-leavens-dhara.pdf}, annote = {A survey of behavioral subtyping. 79 references.} } @TechReport{Leavens-Dhara92, Key = "Leavens \& Dhara", Author = "Gary T. Leavens and Krishna Kishore Dhara", Title = "A Foundation for the Model Theory of Abstract Data Types with Mutation and Aliasing (preliminary version)", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "92-35", Year = 1992, Month = Nov, Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "14 references." } @TechReport{Leavens-Dhara94, Key = "Leavens \& Dhara", Author = "Gary T. Leavens and Krishna Kishore Dhara", Title = "Blended Algebraic and Denotational Semantics for {ADT} Languages", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "93-21b", Year = 1994, Month = Sep, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-21/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "32 references." } @TechReport{Leavens-Leino-Mueller06, key = {Leavens \& Leino \& M{\"u}ller}, author = {Gary T. Leavens and K. Rustan M. Leino and Peter M{\"u}ller}, title = {Specification and verification challenges for sequential object-oriented programs}, institution = {Department of Computer Science, Iowa State University}, year = 2006, number = {06-14}, address = {Ames, Iowa}, month = {May}, annote = {100 references}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-14/TR.pdf} } @InProceedings{Leavens-Millstein98, Key = "Leavens \& Millstein", Author = "Gary T. Leavens and Todd D. Millstein", Title = "Multiple Dispatch as Dispatch on Tuples", BookTitle = "OOPSLA '98 Conference Proceedings", Series = SIGPLAN, Volume = "33(10)", Month = Oct, Year = 1998, Pages = "374-387", Annote = "36 references.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-03/TR.ps.gz" } @TechReport{Leavens-Millstein98b, Key = "Leavens \& Millstein", Author = "Gary T. Leavens and Todd D. Millstein", Title = "Multiple Dispatch as Dispatch on Tuples", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "98-03b", Year = 1998, Month = July, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-03/TR.ps.gz", Note = "Appears in OOPSLA '98, pp. 374-387. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "37 references." } @Article{Leavens-Nierstrasz-Sitaraman98, key = {Leavens \& Nierstrasz \& Sitaraman}, author = {Gary T. Leavens and Oscar Nierstrasz and Murali Sitaraman}, title = {1997 Workshop on Foundations of Component-Based Systems}, year = 1998, month = Jan, journal = SIGSOFT, volume = 23, number = 1, pages = "38-41", annotate = "8 references." } @Article{Leavens-Pigozzi00, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "A Complete Algebraic Characterization of Behavioral Subtyping", Journal = "Acta Informatica", Year = 2000, Volume = 36, Pages = "617-663", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-15/TR.ps.gz", Annote = "27 references." } @TechReport{Leavens-Pigozzi02, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "Equational Reasoning with Subtypes", Institution = "Department of Computer Science, Iowa State University", Year = 2002, Number = "02-07", Address = "Ames, Iowa, 50011", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-07/TR.ps.gz", Annote = "38 references." } @TechReport{Leavens-Pigozzi91, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "Typed Homomorphic Relations Extended with Subtypes", Institution = "Department of Computer Science, Iowa State University", Year = 1991, Number = "91-14", Address = "Ames, Iowa, 50011", Month = Jun, Note = "Appears in the proceedings of {\em Mathematical Foundations of Programming Semantics '91}, Springer-Verlag, Lecture Notes in Computer Science, volume 598, pages 144-167, 1992.", Annote = "17 references." } @InCollection{Leavens-Pigozzi92, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "Typed Homomorphic Relations Extended with Subtypes", BookTitle = "Mathematical Foundations of Programming Semantics '91", Publisher = "Springer-Verlag", Year = 1992, Editor = "Stephen Brookes", Series = LNCS, Volume = 598, Pages = "144-167", Address = NY, Annote = "17 references." } @TechReport{Leavens-Pigozzi96a, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "The Behavior-Realization Adjunction and Generalized Homomorphic Relations", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "94-18b", Month = Jul, Year = 1996, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-18/TR.ps.Z", Note = "Appears in {\it Theoretical Computer Science}, 177:183-216, 1977." } @TechReport{Leavens-Pigozzi96b, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "An Exact Algebraic Characterization of Behavioral Subtyping", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "96-15", Month = Nov, Year = 1996, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-15/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu" } @Article{Leavens-Pigozzi97, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "The behavior-realization adjunction and generalized homomorphic relations", Journal = TCS, Volume = 177, Year = 1997, Pages = "183-216", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-18/TR.ps.Z", Annote = "25 references." } @TechReport{Leavens-Pigozzi98, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "Class-Based and Algebraic Models of Objects", Institution = "Department of Computer Science, Iowa State University", Year = 1998, Number = "98-02", Address = "Ames, Iowa, 50011", Month = Apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-02/TR.ps.gz", Annote = "52 references." } @InProceedings{Leavens-Pigozzi99, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "Class-Based and Algebraic Models of Objects", Editor = "Rance Cleaveland and Michael Mislove and Philip Mulry", BookTitle = "US---Brazil Joint Workshops on the Formal Foundations of Software Systems", Year = 1999, Series = "Electronic Notes in Theoretical Computer Science", Publisher = "Elsevier", Volume = 14, Note = "http://www.sciencedirect.com/science/journal/15710661", Annote = "52 references." } @TechReport{Leavens-Pigozzi99a, Key = "Leavens \& Pigozzi", Author = "Gary T. Leavens and Don Pigozzi", Title = "A Complete Algebraic Characterization of Behavioral Subtyping", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "96-15a", Month = Nov, Year = 1999, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-15/TR.ps.gz", Note = "To appear in Acta Informatica, 2000." } @TechReport{Leavens-Ruby97, Key = "Leavens \& Ruby", Author = "Gary T. Leavens and Clyde Ruby", Title = "Specification Facets for More Precise, Focused Documentation", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "97-04", Month = Jan, Year = 1997, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-04/TR.ps.gz", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu" } @Book{Leavens-Sitaraman00, title = {Foundations of Component-Based Systems}, year = 2000, key = {Leavens \& Sitaraman}, editor = {Gary T. Leavens and Murali Sitaraman}, publisher = {Cambridge University Press}, address = NY, ISBN = {0-521-77164-1} } @Proceedings{Leavens-Sitaraman97, title = {Foundations of Component-Based Systems Workshop}, year = 1997, key = {Leavens \& Sitaraman}, editor = {Gary T. Leavens and Murali Sitaraman}, month = Sep, note = {Available from http://www.cs.iastate.edu/\verb|~|leavens/FoCBS.} } @Article{Leavens-Vermeulen92, Key = "Leavens-Vermeulen", Author = "Gary T. Leavens and Mike Vermeulen", Title = "$3x+1$ Search Programs", Journal = "Computers and Mathematics with Applications", Month = Dec, Year = 1992, Volume = 24, Number = 11, Pages = "79-99", Annote = "11 references." } @TechReport{Leavens-Wahls-Baker96, Key = "Leavens \& Wahls \& Baker", Author = "Gary T. Leavens and Tim Wahls and Albert L. Baker", Title = "Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages", Institution = "Iowa State University, Department of Computer Science", Year = 1996, Number = "96-16", Month = Dec, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-16/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "47 references." } @InProceedings{Leavens-Wahls-Baker99, author = {Gary T. Leavens and Tim Wahls and Albert L. Baker}, title = {Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages}, booktitle = {ACM SAC'99 -- 1999 ACM Symposium on Applied Computing, San Antonio, Texas}, key = {Leavens \& Wahls \& Baker}, year = 1999, organization = ACM, pages = {526-532}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-16/TR.ps.Z", } @InProceedings{Leavens-Weihl90, Key = "Leavens \& Weihl", Author = "Gary T. Leavens and William E. Weihl", Title = "Reasoning about Object-oriented Programs that use Subtypes (extended abstract)", BookTitle = "{OOPSLA ECOOP '90 Proceedings}", Editor = "N. Meyrowitz", Series = SIGPLAN, Volume = "25(10)", Month = Oct, Year = 1990, Pages = "212-223", Organization = ACM, Annote = "26 references." } @TechReport{Leavens-Weihl93, Key = "Leavens \& Weihl", Author = "Gary T. Leavens and William E. Weihl", Title = "Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "92-28d", Month = Aug, Year = 1994, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR92-28/TR.ps.Z", Note = "Full version of a paper in {\em Acta Informatica}, volume 32, number 8, pages 705--778. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "The journal version of the first author's thesis." } @Article{Leavens-Weihl95, author = {Gary T. Leavens and William E. Weihl}, title = {Specification and Verification of Object-Oriented Programs Using Supertype Abstraction}, journal = {Acta Informatica}, year = 1995, key = {Leavens \& Weihl}, volume = 32, number = 8, month = Nov, pages = {705-778} } @TechReport{Leavens-Wing97, Key = "Leavens \& Wing", Author = "Gary T. Leavens and Jeannette M. Wing", Title = "Protective Interface Specifications", Institution = "Iowa State University, Department of Computer Science", Year = 1997, Number = "96-04d", Month = Sep, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-04/TR.ps.gz", Note = "In Michel Bidoit and Max Dauchet (editors), TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France. Volume 1214 of Lecture Notes in Computer Science, Springer-Verlag, 1997, pages 520-534. Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "29 references." } @InCollection{Leavens-Wing97a, Key = "Leavens \& Wing", Author = "Gary T. Leavens and Jeannette M. Wing", Title = "Protective Interface Specifications", BookTitle = "{TAPSOFT '97}: Theory and Practice of Software Development, 7th International Joint Conference {CAAP/FASE}, Lille, France", Publisher = "Springer-Verlag", Year = 1997, Editor = "Michel Bidoit and Max Dauchet", Series = LNCS, Volume = 1214, Pages = "520-534", Address = NY, Annote = "29 references.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-04/TR.ps.gz" } @Article{Leavens-Wing98, key = {Leavens \& Wing}, author = {Gary T. Leavens and Jeannette M. Wing}, title = {Protective Interface Specifications}, journal = {Formal Aspects of Computing}, year = 1998, volume = 10, pages = {59-75}, annote = {30 references.} } @InProceedings{Leavens-etal00, Key = "Leavens, {\em et al.}", Author = "Gary T. Leavens and K. Rustan M. Leino and Erik Poll and Clyde Ruby and Bart Jacobs", Title = "{JML}: notations and tools supporting detailed design in {Java}", BookTitle = "OOPSLA 2000 Companion, Minneapolis, Minnesota", Year = 2000, Month = Oct, Pages = "105-106", Organization = ACM, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-15/TR.ps.gz", Annote = "Abstract of an OOPSLA 2000 poster. 14 references." } @TechReport{Leavens-etal00a, Key = "Leavens, {\em et al.}", Author = "Gary T. Leavens and K. Rustan M. Leino and Erik Poll and Clyde Ruby and Bart Jacobs", Title = "{JML}: notations and tools supporting detailed design in {Java}", Institution = "Iowa State University, Department of Computer Science", Year = 2000, Number = "00-15", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-15/TR.ps.gz", Note = "Appears in OOPSLA '00 Companion, pp. 105--106", Annote = "Abstract of an OOPSLA 2000 poster. 14 references." } @InProceedings{Leavens-etal01, author = {Gary T. Leavens and Sophia Drossopoulou and Susan Eisenbach and Arnd Poetzsch-Heffter and Erik Poll}, title = {Formal Techniques for {J}ava Programs}, booktitle = {Object-Oriented Technology. {ECOOP} 2001 Workshop Reader}, year = 2001, editor = {A. Frohner}, series = LNCS, volume = 2323, publisher = {Springer-Verlag}, pages = {30-40} } @Unpublished{Leavens-etal02, Key = {Leavens \& Poll \& Clifton \& Cheon \& Ruby}, Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby}, Title = {JML Reference Manual}, Month = Aug, Year = 2002, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @Unpublished{Leavens-etal03, Key = {Leavens \& Poll \& Clifton \& Cheon \& Ruby}, Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David R. Cok and Joseph Kiniry}, Title = {JML Reference Manual}, Month = Apr, Year = 2003, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @InCollection{Leavens-etal03a, Key = {Leavens, {\em et al.}}, Author = {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton and Clyde Ruby and David R. Cok}, Title = {How the Design of {JML} Accommodates Both Runtime Assertion Checking and Formal Verification}, BookTitle = {Formal Methods for Components and Objects: First International Symposium, FMCO 2002, Lieden, The Netherlands, November 2002, Revised Lectures}, Year = 2003, Editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem-Paul de Roever}, Series = LNCS, Volume = 2852, Publisher = "Springer-Verlag", Address = "Berlin", Pages = "262-284", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-04/TR.pdf", Annote = "81 references." } @TechReport{Leavens-etal03b, Key = {Leavens, {\em et al.}}, Author = {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton and Clyde Ruby and David R. Cok}, Title = {How the Design of {JML} Accommodates Both Runtime Assertion Checking and Formal Verification}, Institution = "Department of Computer Science, Iowa State University", Year = 2003, Number = "03-04", Address = "Ames, Iowa, 50011", Month = Mar, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-04/TR.pdf", Note = "Published in FMCO 2002 proceedings, LNCS 2852, 2003.", Annote = "81 references." } @Unpublished{Leavens-etal04a, Key = {Leavens \& Poll \& Clifton \& Cheon \& Ruby}, Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David R. Cok and Joseph Kiniry}, Title = {JML Reference Manual}, Month = Jul, Year = 2004, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @Article{Leavens-etal05, Key = {Leavens, {\em et al.}}, Author = {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton and Clyde Ruby and David R. Cok}, Title = {How the Design of {JML} Accommodates Both Runtime Assertion Checking and Formal Verification}, Journal = {Science of Computer Programming}, Year = 2005, Month = Mar, Volume = 55, Number = {1-3}, Publisher = {Elsevier}, Pages = {185-208} } @Unpublished{Leavens-etal05a, Key = {Leavens, {\em et al.}}, Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David R. Cok and Peter M\"{u}ller and Joseph Kiniry}, Title = {{JML} Reference Manual}, Month = Jul, Year = 2005, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @Unpublished{Leavens-etal06, Key = {Leavens, {\em et al.}}, Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David R. Cok and Peter M\"{u}ller and Joseph Kiniry and Patrice Chalin}, Title = {{JML} Reference Manual}, Month = Jan, Year = 2006, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @TechReport{Leavens-etal96, Key = "Leavens, {\em et al.}", Author = "Gary T. Leavens and Tim Wahls and Albert L. Baker and Kari Lyle", Title = "An Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams", Institution = "Iowa State University, Department of Computer Science", Year = 1996, Number = "93-28d", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-28/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "43 references." } @Article{Leavens-etal98, Key = "Leavens, {\em et al.}", Author = "Gary T. Leavens and Albert L. Baker and Vasant Honavar and Steven Lavalle and Gurpur Prabhu", Title = "Programming is Writing: Why Student Programs must be Carefully Evaluated", Journal = "Mathematics and Computer Education", Institution = "Iowa State University, Department of Computer Science", Year = 1998, Volume = 32, Number = 3, Pages = "284-295", Month = "Fall", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-23/TR.ps.gz" } @TechReport{Leavens-etal98a, Key = "Leavens, {\em et al.}", Author = "Gary T. Leavens and Albert L. Baker and Vasant Honavar and Steven Lavalle and Gurpur Prabhu", Title = "Programming is Writing: Why Student Programs must be Carefully Read", Institution = "Iowa State University, Department of Computer Science", Year = 1998, Number = "97-23a", Month = Jun, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-23/TR.ps.gz" } @Article{Leavens00, author = {Gary T. Leavens}, title = {Formal Methods for Multimethod Software Components}, journal = {Software Engineering Notes}, year = 2000, key = {Leavens}, volume = 25, number = 1, pages = {62-63}, month = Jan } @Article{Leavens84, Key = "Leavens", Author = "Gary T. Leavens", Title = "Bibliography on Data Types", Journal = SIGPLAN, Year = 1984, Volume = 19, Number = 8, Month = Aug, Pages = "41-50", Annote = "Hundreds of annotated references, but the bibliography is not selective and gives the reader no direction." } @PhDThesis{Leavens88, Key = "Leavens", Author = "Gary Todd Leavens", Title = "Verifying Object-Oriented Programs that use Subtypes", Month = Dec, Year = 1988, School = MIT, Note = "Published as MIT/LCS/TR-439 in February 1989.", Annote = "44 references." } @TechReport{Leavens89, Key = "Leavens", Author = "Gary Todd Leavens", Title = "Verifying Object-Oriented Programs that use Subtypes", Month = Feb, Year = 1989, Institution = MITLCS, Number = 439, Note = "The author's Ph.D. thesis.", Annote = "44 references." } @TechReport{Leavens89b, Key = "Leavens", Author = "Gary T. Leavens", Title = "A Distributed Search Program for the $3x+1$ problem", Institution = "Iowa State University, Department of Computer Science", Year = 1989, Number = "89-22", Address = "Ames, Iowa", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR89-22/TR.ps.Z", Month = Nov } @TechReport{Leavens06, Key = "Leavens", Author = "Gary T. Leavens", Title = "Following the Grammar", Month = Jan, Year = 2006, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "05-02a", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR05-02/TR.pdf", Note = "Available by anonymous ftp from ftp.cs.iastate.edu.", Annote = "8 references." } @Article{Leavens06a, key = {Leavens}, author = {Gary T. Leavens}, title = {Not a Number of Floating Point Problems}, journal = {Journal of Object Technology}, year = 2006, volume = 5, number = 2, pages = {75-83}, month = {March-April}, note = {\url{http://www.jot.fm/issues/issues_2006_03/column8}}, URL = {\url{http://www.jot.fm/issues/issues_2006_03/column8}} } @TechReport{Leavens90, Key = "Leavens", Author = "Gary T. Leavens", Title = "Modular Verification of Object-Oriented Programs with Subtypes", Month = Jul, Year = 1990, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "90-09", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR90-09/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "Revised thesis. 74 references." } @Article{Leavens91, Key = "Leavens", Author = "Gary T. Leavens", Title = "Modular Specification and Verification of Object-Oriented Programs", Journal = "IEEE Software", Year = 1991, Volume = 8, Number = 4, Month = Jul, Pages = "72-80", Annote = "8 references." } @Article{Leavens91b, Key = "Leavens", Author = "Gary T. Leavens", Title = "Introduction to the Literature on Object-Oriented Design, Programming, and Languages", Journal = "OOPS Messenger", Year = 1991, Volume = 2, Number = 4, Month = Oct, Annote = "Hundreds of references." } @TechReport{Leavens93b, Key = "Leavens", Author = "Gary T. Leavens", Title = "Inheritance of Interface Specifications (Extended Abstract)", Institution = "Iowa State University, Department of Computer Science", Year = 1993, Number = "93-23", Month = Sep, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-23/TR.ps.Z", Note = "Appears in the Workshop on Interface Definition Languages, WIDL '94.", Annote = "28 references." } @InProceedings{Leavens94a, Key = "Leavens", Author = "Gary T. Leavens", Title = "Inheritance of Interface Specifications (Extended Abstract)", BookTitle = "Proceedings of the Workshop on Interface Definition Languages.", Series = SIGPLAN, Year = 1994, Volume = "29(8)", Pages = "129-138", Month = Aug, Annote = "28 references." } @TechReport{Leavens94b, Key = "Leavens", Author = "Gary T. Leavens", Title = "Fields in Physics are like Curried Functions or Physics for Functional Programmers", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "94-06b", Year = 1994, Month = May, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-06/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu", Annote = "20 references." } @TechReport{Leavens94c, Key = "Leavens", Author = "Gary T. Leavens", Title = "Introduction to the Literature on Semantics", Institution = "Iowa State University, Department of Computer Science", Year = 1994, Number = "94-15", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-15/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "Many references." } @Article{Leavens95, key = "Leavens", author = "Gary T. Leavens", title = "Aiding Self-motivation with Readings in Introductory Computing", journal = "Mathematics and Computer Education", year = 1995, volume = 29, number = 2, pages = "124-133", month = "Spring", annote = "40 references" } @TechReport{Leavens95b, key = "Leavens", author = "Gary T. Leavens", title = "A Physical Example for Teaching Curried Functions", institution = "Department of Computer Science, Iowa State University", year = 1995, number = "95-05", address = "Ames, Iowa, 50011", month = Mar, note = "Appears in {\it Mathematics and Computer Education}, volume 30, number 1, pages 51-60. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu" } @Article{Leavens96a, key = "Leavens", author = "Gary T. Leavens", title = "A Physical Example for Teaching Curried Functions", journal = "Mathematics and Computer Education", year = 1996, volume = 30, number = 1, pages = "51-60", month = "Winter", annote = "15 references" } @InCollection{Leavens96b, key = "Leavens", author = "Gary T. Leavens", title = "An Overview of {Larch/C++}: Behavioral Specifications for {C++} Modules", booktitle = "Specification of Behavioral Semantics in Object-Oriented Information Modeling", publisher = "Kluwer Academic Publishers", year = 1996, address = "Boston", editor = "Haim Kilov and William Harvey", institution = "Department of Computer Science, Iowa State University", chapter = 8, pages = "121-142", annote = "52 references.", note = "An extended version is TR \#96-01b, Department of Computer Science, Iowa State University, Ames, Iowa, 50011" } @TechReport{Leavens96f, key = "Leavens", author = "Gary T. Leavens", title = "An Overview of {Larch/C++}: Behavioral Specifications for {C++} Modules", institution = "Department of Computer Science, Iowa State University", year = 1996, number = "96-01b", address = "Ames, Iowa, 50011", month = Apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.Z", note = "Appears in Haim Kilov and William Harvey, editors, {\it Specification of Behavioral Semantics in Object-Oriented Information Modeling\/} (Kluwer Academic Publishers, 1996), Chapter 8, pages 121--142. Available by anonymous ftp from ftp.cs.iastate.edu, and by e-mail from almanac@cs.iastate.edu.", annote = "52 references." } @Unpublished{Leavens97c, Key = "Leavens", Author = "Gary T. Leavens", Title = "{Larch/C++ Reference Manual}", URL = "ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz", Note = "Version 5.14. Available in ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz or on the World Wide Web at the URL http://www.cs.iastate.edu/\verb|~|leavens/larchc++.html", Annote = "Definitive reference on Larch/C++. Many references.", Month = Oct, Year = 1997 } @TechReport{Leavens97d, key = "Leavens", author = "Gary T. Leavens", title = "An Overview of {Larch/C++}: Behavioral Specifications for {C++} Modules", Institution = "Iowa State University, Department of Computer Science", note = "Revised version of Haim Kilov and William Harvey, {\it Specification of Behavioral Semantics in Object-Oriented Information Modeling}, chapter 8, pages 121--142. Kluwer Academic Publishers, Boston, 1996.", annote = "52 references.", Year = 1997, Number = "96-01d", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.gz", } @Unpublished{Leavens99, Key = "Leavens", Author = "Gary T. Leavens", Title = "{Larch/C++ Reference Manual}", URL = "ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz", Note = "Version 5.41. Available in ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz or on the World Wide Web at the URL http://www.cs.iastate.edu/\verb|~|leavens/larchc++.html", Annote = "Definitive reference on Larch/C++. Many references.", Month = Apr, Year = 1999 } @InCollection{Leavens99a, author = {Gary T. Leavens}, title = {Abstract Data Types}, editor = {John G. Webster}, booktitle = {Wiley Encyclopedia of Electrical and Electronics Engineering}, publisher = {John Wiley \& Sons, Inc.}, year = 1999, key = {Leavens}, volume = 1, pages = {4-14}, URL = "http://www.wiley.com/products/subject/engineering/webster/WEBSTER_PG4-25_A1.pdf", annote = {23 references.} } @TechReport{Leavens99b, Key = "Leavens", Author = "Gary T. Leavens", Title = "Introduction to the Literature On Programming Language Design", Institution = "Iowa State University, Department of Computer Science", Year = 1999, Number = "93-01c", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-01/TR.ps.gz", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "Many references." } @Unpublished{Leavens:LarchFAQ, Key = "Leavens", Author = "Gary T. Leavens", Title = "{Larch} Frequently Asked Questions", Note = "Version 1.110. Available in http://www.cs.iastate.edu/\verb|~|leavens/larch-faq.html", Annote = "Beginner's guide to Larch, LSL, LP. Many references.", Month = May, Year = 2000, URL = "http://www.cs.iastate.edu/~leavens/larch-faq.html" } @TechReport{Liskov-etal83, Key = "Liskov, {\em et al.}", Author = "Barbara Liskov and Maurice Herlihy and Paul Johnson and Gary Leavens and Robert Scheifler and William Weihl", Title = "Preliminary Argus Reference Manual", Type = "Programming Methodology Group Memo", Number = 39, Month = Oct, Institution = MITLCS, Year = 1983, Annote = "Describes only the differences from CLU. 3 references." } @TechReport{Liskov-etal87, Key = "Liskov, {\em et al.}", Author = "Barbara Liskov and Mark Day and Maurice Herlihy and Paul Johnson and Gary Leavens and Robert Scheifler and William Weihl", Title = "Argus Reference Manual", Number = 400, Month = Oct, Institution = MITLCS, Year = 1987, Note = "An earlier version appeared as Programming Methodology Group Memo 54 in March 1987." } @TechReport{Mueller-Poetzsch-Heffter-Leavens01, Key = {M\"{u}ller \& Poetzsch-Heffter \& Leavens}, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Specification of Frame Properties in JML", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "01-03", Year = 2001, Month = Apr, Note = "To appear in the Formal Techniques for Java Programs 2001 workshop at ECOOP 2001. Also available from archives.cs.iastate.edu.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR01-03/TR.pdf", Annote = "18 references." } @TechReport{Mueller-Poetzsch-Heffter-Leavens02, Key = {M\"{u}ller \& Poetzsch-Heffter \& Leavens}, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Specification of Frame Properties in {JML}", Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "02-02a", Year = 2002, Month = Oct, Note = "To appear in Concurrency, Computation Practice and Experience.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf", Annote = "31 references." } @Article{Mueller-Poetzsch-Heffter-Leavens03, Key = {M\"{u}ller \& Poetzsch-Heffter \& Leavens}, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Specification of Frame Properties in {JML}", Journal = "Concurrency, Computation Practice and Experience.", Volume = 15, Year = 2003, Pages = "117-154", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf", Annote = "31 references." } @TechReport{Mueller-Poetzsch-Heffter-Leavens03a, Key = {M\"{u}ller \& Poetzsch-Heffter \& Leavens}, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Invariants for Object Structures", institution = {ETH Zurich}, year = 2003, number = 424, month = Oct, annote = {20 references}, URL = {http://www.inf.ethz.ch/research/dissertations/data/tech-reports/4xx/424.pdf} } @TechReport{Mueller-Poetzsch-Heffter-Leavens05, Key = {M\"{u}ller \& Poetzsch-Heffter \& Leavens}, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Invariants for Layered Object Structures", institution = {ETH Zurich}, year = 2005, number = 424, month = Mar, annote = {20 references}, URL = {http://sct.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=MuellerPoetzsch-HeffterLeavens03a.pdf} } @TechReport{Raghavan-Leavens05, Key = "Raghavan \& Leavens", Author = "Arun D. Raghavan and Gary T. Leavens", Title = "Desugaring {JML} Method Specifications", Institution = "Iowa State University, Department of Computer Science", Year = 2005, Number = "00-03e", Month = May, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.pdf", Annote = "31 references." } @InCollection{Rodriguez-etal05, key = {Rodriguez, {\em et al.}}, author = {Edwin Rodr\'{i}guez and Matthew B. Dwyer and Cormac Flanagan and John Hatcliff and Gary T. Leavens and Robby}, title = {Extending {JML} for Modular Specification and Verification of Multi-Threaded Programs}, booktitle = {ECOOP 2005 --- Object-Oriented Programming 19th European Conference, Glasgow, UK}, pages = {551-576}, year = 2005, editor = {Andrew P. Black}, volume = 3586, series = LNCS, address = {Berlin}, month = Jul, publisher = {Springer-Verlag}, annote = {39 references.} } @TechReport{Rodriguez-etal05a, key = {Rodriguez, {\em et al.}}, author = {Edwin Rodr\'{i}guez and Matthew B. Dwyer and Cormac Flanagan and John Hatcliff and Gary T. Leavens and Robby}, title = {Extending {JML} for Modular Specification and Verification of Multi-Threaded Programs}, institution = {Kansas State University, Department of Computing and Information Sciences}, year = 2005, number = {SAnToS-TR2004-10}, month = May, annote = {39 references.}, note = {To appear in \textit{ECOOP 2005}.}, URL = {http://spex.projects.cis.ksu.edu/papers/SAnToS-TR2004-10.pdf} } @InProceedings{Ruby-Leavens00, Key = "Ruby \& Leavens", Author = "Clyde Ruby and Gary T. Leavens", Title = "Safely Creating Correct Subclasses without Seeing Superclass Code", BookTitle = "OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota", Series = SIGPLAN, Volume = "35(10)", Month = Oct, Year = 2000, Pages = "208-228", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-05/TR.ps.gz", Annote = "39 references." } @TechReport{Ruby-Leavens00a, Key = "Ruby \& Leavens", Author = "Clyde Ruby and Gary T. Leavens", Title = "Safely Creating Correct Subclasses without Seeing Superclass Code", Institution = "Iowa State University, Department of Computer Science", Year = 2000, Number = "00-05d", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-05/TR.ps.gz", Note = "Appears in OOPSLA 2000 Conference Proceedings, pp. 208--228.", Annote = "39 references." } @TechReport{Wahls-Baker-Leavens93, Key = "Wahls \& Baker \& Leavens", Author = "Tim Wahls and Albert L. Baker and Gary T. Leavens", Title = "An Executable Semantics for a Formalized Data Flow Diagram Specification Language", Institution = "Department of Computer Science, Iowa State University", Year = 1993, Number = "93-27", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Nov, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-27/TR.ps.Z", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.", Annote = "21 references." } @Article{Wahls-Leavens-Baker00, key = "Wahls \& Leavens \& Baker", author = "Tim Wahls and Gary T. Leavens and Albert L. Baker", title = "Executing Formal Specifications with Concurrent Constraint Programming", journal = "Automated Software Engineering", volume = 7, number = 4, month = Dec, pages = "315 - 343", year = 2000, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-12/TR.ps.gz" } @TechReport{Wahls-Leavens-Baker00a, Key = "Wahls \& Leavens \& Baker", Author = "Tim Wahls and Gary T. Leavens and Albert L. Baker", Title = "Executing Formal Specifications with Constraint Programming", Institution = "Department of Computer Science, Iowa State University", Year = 2000, Number = "97-12c", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Jul, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR97-12/TR.ps.gz", Note = "In {\em Automated Software Engineering}, volume 7, number 4, pp 315--343, December 2000." } @TechReport{Wahls-Leavens00, Key = "Wahls \& Leavens", Author = "Tim Wahls and Gary T. Leavens", Title = "Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs", Institution = "Department of Computer Science, Iowa State University", Year = 2000, Number = "00-02a", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = Aug, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR00-02/TR.ps.gz", Note = "Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu." } @InProceedings{Wahls-Leavens01, Key = "Wahls \& Leavens", Author = "Tim Wahls and Gary T. Leavens", Title = "Formal Semantics of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs", booktitle = {Proceedings of the 16th ACM Symposium on Applied Computing, Las Vegas, Nevada}, pages = {567-575}, year = 2001, month = Mar, organization = ACM } @InProceedings{deChampeaux-etal91, Key = "deChampeaux, {\em et al.}", Author = "Dennis de Champeaux and Pierre America and Derek Coleman and Roger Duke and Doug Lea and Gary Leavens", Title = "Formal Techniques for {OO} Software Development", BookTitle = "OOPSLA '92 Proceedings", Editor = "Andreas Paepcke", Series = SIGPLAN, Year = 1991, Volume = "26(11)", Month = Nov, Pages = "166-170", Annote = "no references" }