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.178 2007/10/25 12:21:05 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: 2007/10/25 12:21:05 $", %%% filename = "leavens.bib", %%% url = "ftp://ftp.cs.iastate.edu/pub/leavens/leavens.bib", %%% www-home = "http://www.eecs.ucf.edu/~leavens/", %%% address = "School of EECS - Bldg. 116, %%% University of Central Florida, %%% 4000 Central Florida Blvd., %%% Orlando, FL 32816-2362 USA", %%% telephone = "+1 407 823-4758", %%% FAX = "+1 407 823-5419", %%% FTP-archive = "ftp://ftp.cs.iastate.edu/pub/leavens/", %%% email = "leavens@eecs.ucf.edu", %%% dates = {1980--}, %%% keywords = "type, specification, verification, object-oriented", %%% supported = "yes", %%% supported-by = "Gary T. Leavens ", %%% abstract = "Bibliography for Gary T. Leavens" %%% } %%% ==================================================================== @TechReport{Assaad-Leavens01, 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, 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, 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, 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, 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, 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, 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 = SV, pages = {212--232}, URL = {http://dx.doi.org/10.1007/s10009-004-0167-4}, annotate = {93 references.} } @Article{Castagna-Leavens95, 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{Chalin-etal06, author = {Patrice Chalin and Joseph R. Kiniry and Gary T. Leavens and Erik Poll}, title = {Beyond Assertions: Advanced Specification and Verification with {JML} and {ESC/Java2}}, booktitle = {Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures}, year = 2006, series = LNCS, volume = 4111, publisher = SV, pages = {342-363}, URL = {http://dx.doi.org/10.1007/11804192_16} } @InProceedings{Chambers-Leavens94, 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, 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, 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, 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", journal = "TOPLAS", year = 1995, volume = 17, number = 6, pages = "805-843", month = nov, annote = "56 references." } @InProceedings{Chambers-Leavens96, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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}, URL = {http://doi.acm.org/10.1145/1085130.1085150}, annote = {30 references.} } @TechReport{Cheon-Leavens05a, 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, 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, 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, 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, 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, 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, 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 = "In \emph{Software -- Practice \& Experience}, 35(6):583--599, May 2005. Available from \url{archives.cs.iastate.edu}.", Annote = "39 references." } @TechReport{Cheon-etal04, 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 = "In \emph{Software -- Practice \& Experience}, 35(6):583--599, May 2005. Available from \url{archives.cs.iastate.edu}.", Annote = "26 references." } @Article{Cheon-etal05, 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", doi = "http://dx.doi.org/10.1002/spe.649", Annote = "DOE: 10.1002/see.649" } @TechReport{Clifton-Leavens-Wand03, 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, 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, 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, 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 Reports}, number = {02-06}, month = apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-06/TR.pdf" } @TechReport{Clifton-Leavens02b, 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, 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, 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}, 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, 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, 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.} } @Article{Clifton-Leavens06, author = {Curtis Clifton and Gary T. Leavens}, title = {{MiniMAO}$_1$: Investigating the Semantics of Proceed}, month = dec, year = 2006, journal = SCP, publisher = {Elsevier}, volume = 63, number = 3, pages = {321-374}, URL = {http://dx.doi.org/10.1016/j.scico.2006.02.009}, annote = {17 references.} } @InProceedings{Clifton-Leavens-Noble07, author = {Curtis Clifton and Gary T. Leavens and James Noble}, title = {MAO: Ownership and Effects for more Effective Reasoning about Aspects}, booktitle = {ECOOP 2007 --- Object-Oriented Programming, 21st European Conference, Berlin, Germany, Proceedings}, pages = {451-475}, editor = {Erik Ernst}, volume = 4609, series = LNCS, address = {Berlin}, publisher = {Springer-Verlag}, year = 2007, month = jul, URL = "http://dx.doi.org/10.1007/978-3-540-73589-2_22", annote = {32 references.} } @TechReport{Clifton-Leavens-Noble07a, author = {Curtis Clifton and Gary T. Leavens and James Noble}, title = {MAO: Ownership and Effects for more Effective Reasoning about Aspects}, year = 2007, number = {06-35a}, address = {Ames, IA, 50011}, month = apr, institution = {Dept. of Computer Science, Iowa State University}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR06-35/TR.pdf", note = {In {\em ECOOP 2007}, Springer-Verlag LNCS Volume 4609, pages 451--475.}, annote = {32 references.} } @InProceedings{Clifton-etal00, 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, 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, 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 = "Appears in ACM TOPLAS, vol 28, number 3, May 2006.", annote = {many references} } @Article{Clifton-etal06, author = {Curtis Clifton and Todd Millstein and Gary T. Leavens and Craig Chambers}, title = {{MultiJava}: Design Rationale, Compiler Implementation, and Applications}, journal = TOPLAS, volume = 28, number = 3, month = may, pages = {517-575}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR04-01/TR.pdf}, year = {2006}, annote = {80 references}, doi = {http://doi.acm.org/10.1145/1133651.1133655} } @TechReport{Dhara-Leavens01, 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, 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, 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, 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, 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, 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, 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 ISU CS TR \#95-20c, \url{http://tinyurl.com/s2krg}.", Annote = "19 references." } @TechReport{Dorn-Leavens07, author = {Brian Dorn and Gary T. Leavens}, title = {A Framework for Implementing Type Systems}, institution = {Department of Computer Science, Iowa State University}, year = 2007, number = {07-12}, address = {226 Atanasoff Hall, Ames, Iowa 50011}, month = jul, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR07-12/TR.pdf}, annote = {Typedscm. 13 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, 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, volume = 13, number = 13, pages = {1121-1123} } @InCollection{Eisenbach-etal04, author = {Susan Eisenbach and Gary T. Leavens and Peter M\"{u}ller and Arnd Poetzsch-Heffter and Erik Poll}, title = {Formal Techniques for {Java}-Like Programs}, booktitle = {Object-Oriented Technology ECOOP 2003 Workshop Reader}, pages = {62-71}, publisher = SV, year = 2004, editor = {Frank Buschmann and Alejandro P. Buschmann and Mariano A. Cilia}, volume = 3013, series = LNCS, address = NY, annote = {6 references.} } @Proceedings{FOAL02, 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, 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, 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, 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, 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{Khanolkar-Leavens06, author = {Neeraj Khanolkar and Gary T. Leavens}, title = {Executable Documentation of Template-Hook Interactions in Frameworks using JML}, institution = "Department of Computer Science, Iowa State University", year = 2006, number = {06-18}, address = {Ames, Iowa}, month = jun, annote = {18 references.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-18/TR.pdf} } @TechReport{Kulczycki-etal02, 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, 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, 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" } @Article{Leavens-Baker-Ruby06, Author = "Gary T. Leavens and Albert L. Baker and Clyde Ruby", Title = "Preliminary Design of {JML}: A Behavioral Interface Specification Language for {Java}", journal = SIGSOFT, volume = 31, number = 3, month = mar, year = 2006, pages = {1-38}, URL = {\url{http://doi.acm.org/10.1145/1127878.1127884}}, publisher = ACM, address = NY } @TechReport{Leavens-Baker-Ruby06a, 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 = "Also \emph{ACM SIGSOFT Software Engineering Notes}, 31(3):1-38, March 2006." } @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)}, year = 1998, month = oct, note = {{\tt http://www-dse.doc.ic.ac.uk/{\char'176}sue/oopsla/cfp.html}} } @InCollection{Leavens-Baker-Ruby99b, 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, 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 = "http://tinyurl.com/qv84o", Annote = "37 references." } @TechReport{Leavens-Baker99a, 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, 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, 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, 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, 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, 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, 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-Clifton-Dorn06, 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." } @TechReport{Leavens-Clifton05, author = {Gary T. Leavens and Curtis Clifton}, title = {A Type Notation for {Scheme}}, 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." } @InProceedings{Leavens-Clifton05a, author = {Gary T. Leavens and Curtis Clifton}, title = {Lessons from the {JML} Project}, year = 2005, booktitle = {Verified Software: Theories, Tools, Experiments, Zurich, Switzerland}, editor = {Bertrand Meyer and Jim Woodcock}, month = oct, publisher = SV, volume = 4171, series = LNCS, 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}, 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-Clifton07, Author = "Gary T. Leavens and Curtis Clifton", Title = "Multiple Concerns in Aspect-Oriented Language Design: A Language Engineering Approach to Balancing Benefits, with Examples", Year = 2007, Month = feb, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "07-01a", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR07-01/TR.pdf", note = {Also in {\em SPLAT 2007}.}, Annote = "26 references." } @InCollection{Leavens-Dhara00, 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, 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, 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." } @InProceedings{Leavens-Kiniry-Poll07, author = {Gary T. Leavens and Joseph R. Kiniry and Erik Poll}, title = {A {JML} Tutorial: Modular Specification and Verification of Functional Behavior for {Java}}, booktitle = {Computer Aided Verification 2007}, pages = 37, year = 2007, editor = {Werner Damm and Holger Hermanns}, volume = 4590, series = LNCS, address = {Berlin}, month = jul, publisher = SV, annote = {3 references.} } @TechReport{Leavens-Leino-Mueller06, 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-14a}, address = {Ames, Iowa}, month = aug, annote = {122 references.}, note = {In {\em Formal Aspects of Computing}, 19(2):159--189.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-14/TR.pdf} } @Article{Leavens-Leino-Mueller07, author = {Gary T. Leavens and K. Rustan M. Leino and Peter M{\"u}ller}, title = {Specification and verification challenges for sequential object-oriented programs}, journal = FAC, volume = 19, number = 2, pages = {159-189}, month = jun, year = 2007, publisher = SV, annote = {122 references.}, URL = {http://dx.doi.org/10.1007/s00165-007-0026-7} } @InProceedings{Leavens-Millstein98, 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", doi = {http://doi.acm.org/10.1145/286936.286977} } @TechReport{Leavens-Millstein98b, 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 = jul, 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." } @TechReport{Leavens-Mueller06, author = {Gary T. Leavens and Peter M{\"u}ller}, title = {Information Hiding and Visibility in Interface Specifications}, institution = {Department of Computer Science, Iowa State University}, year = 2006, number = {06-28}, address = {Ames, Iowa}, month = sep, annote = {32 references}, note = {In ICSE 2007, pages 385-395.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-28/TR.pdf} } @InProceedings{Leavens-Mueller07, author = {Gary T. Leavens and Peter M{\"u}ller}, title = {Information Hiding and Visibility in Interface Specifications}, booktitle = {International Conference on Software Engineering (ICSE)}, pages = {385-395}, year = 2007, month = may, organization = IEEE, annote = {32 references.}, URL = {http://dx.doi.org/10.1109/ICSE.2007.44} } @TechReport{Leavens-Naumann06, author = {Gary T. Leavens and David A. Naumann}, title = {Behavioral Subtyping, Specification Inheritance, and Modular Reasoning}, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "06-20b", year = 2006, month = sep, annote = {50 references.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-20/TR.pdf} } @TechReport{Leavens-Naumann06a, author = {Gary T. Leavens and David A. Naumann}, title = {Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs}, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "06-36", year = 2006, month = dec, annote = {68 references.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-36/TR.pdf} } @TechReport{Leavens-Naumann-Rosenberg06, author = {Gary T. Leavens and David A. Naumann and Stan Rosenberg}, title = {Preliminary Definition of {Core JML}}, Institution = "Stevens Institute of Technology", type = "CS Report", number = "2006-07", year = 2006, month = sep, annote = {11 references.}, URL = {http://www.cs.stevens.edu/~naumann/publications/SIT-TR-2006-07.pdf} } @Article{Leavens-Nierstrasz-Sitaraman98, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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 = "In {\em Acta Informatica}, 36:617-663, 2000." } @TechReport{Leavens-Ruby97, 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, 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, editor = {Gary T. Leavens and Murali Sitaraman}, month = sep, note = {Available from http://www.cs.iastate.edu/\verb|~|leavens/FoCBS.} } @Article{Leavens-Vermeulen92, 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, 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}, year = 1999, organization = ACM, pages = {526-532}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR96-16/TR.ps.Z", } @InProceedings{Leavens-Weihl90, 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, 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, volume = 32, number = 8, month = nov, pages = {705-778}, doi = {http://dx.doi.org/10.1007/BF01178658} } @TechReport{Leavens-Wing97, 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, 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, author = {Gary T. Leavens and Jeannette M. Wing}, title = {Protective Interface Specifications}, journal = {Formal Aspects of Computing}, year = 1998, volume = 10, number = 1, month = jan, pages = {59-75}, annote = {30 references.}, url = {http://dx.doi.org/10.1007/PL00003926} } @InProceedings{Leavens-etal00, 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, 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, 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, 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, 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, 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, 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, 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}, URL = {http://dx.doi.org/10.1016/j.scico.2004.05.015} } @Unpublished{Leavens-etal05a, 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, 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 = aug, Year = 2006, Note = {Department of Computer Science, Iowa State University. Available from {\url{http://www.jmlspecs.org}}} } @InProceedings{Leavens-etal06a, author = {Gary T. Leavens and Jean-Raymond Abrial and Don Batory and Michael Butler and Alessandro Coglio and Kathi Fisler and Eric Hehner and Cliff Jones and Dale Miller and Simon Peyton-Jones and Murali Sitaraman and Douglas R. Smith and Aaron Stump}, title = {Roadmap for Enhanced Languages and Methods to Aid Verification}, booktitle = {Fifth International Conference on Generative Programming and Component Engineering (GPCE)}, pages = {221-235}, year = 2006, month = oct, organization = ACM, URL = {http://doi.acm.org/10.1145/1173706.1173740}, annote = {A VSTTE committee roadmap. 146 references.} } @TechReport{Leavens-etal06b, author = {Gary T. Leavens and Jean-Raymond Abrial and Don Batory and Michael Butler and Alessandro Coglio and Kathi Fisler and Eric Hehner and Cliff Jones and Dale Miller and Simon Peyton-Jones and Murali Sitaraman and Douglas R. Smith and Aaron Stump}, title = {Roadmap for Enhanced Languages and Methods to Aid Verification}, institution = {Iowa State University, Department of Computer Science}, year = 2006, number = {06-21}, address = {Ames, IA}, month = jul, annote = {A VSTTE committee roadmap. 146 references.}, note = {In Proceedings of {\em GPCE'06}, pages 221--235.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-21/TR.pdf} } @Unpublished{Leavens-etal07, 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 = oct, Year = 2007, Note = {Available from \url{http://www.jmlspecs.org}} } @TechReport{Leavens-etal96, 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, 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, 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, volume = 25, number = 1, pages = {62-63}, month = jan } @InProceedings{Leavens04, author = {Gary T. Leavens}, title = {{JML} Framed!}, booktitle = {2004 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE'04)}, pages = 1, year = 2004, month = jun, organization = ACM, annote = {Invited talk abstract.} } @TechReport{Leavens06, 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, 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}} } @InProceedings{Leavens06b, author = {Gary T. Leavens}, title = {{JML's} Rich, Inherited Specifications for Behavioral Subtypes}, booktitle = {Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM)}, pages = {2-34}, year = 2006, editor = {Zhiming Liu and He Jifeng}, volume = 4260, series = LNCS, address = NY, month = nov, publisher = SV, URL = {\url{http://dx.doi.org/10.1007/11901433_2}}, annote = {81 references.} } @TechReport{Leavens06c, author = {Gary T. Leavens}, title = {{JML's} Rich, Inherited Specifications for Behavioral Subtypes}, Institution = "Department of Computer Science, Iowa State University", Address = "Ames, Iowa, 50011", Number = "06-22", year = 2006, month = aug, annote = {81 references.}, note = {Also in the proceedings of {\em ICFEM'06}, LNCS vol 4260, pages 2-34.}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR06-22/TR.pdf} } @Article{Leavens84, 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, 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, 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, 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{Leavens90, 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, 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", URL = {http://dx.doi.org/10.1109/52.300040}, Annote = "8 references." } @Article{Leavens91b, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, 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, volume = 1, pages = {4-14}, URL = "http://www.wiley.com/products/subject/engineering/webster/WEBSTER_PG4-25_A1.pdf", annote = {23 references.} } @TechReport{Leavens99b, 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, 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, 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, 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, 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 = "In 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, 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 = "Final version appears in Concurrency and Computation: Practice and Experience, 15:117-154, 2003.", URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf", Annote = "31 references." } @Article{Mueller-Poetzsch-Heffter-Leavens03, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Specification of Frame Properties in {JML}", Journal = "Concurrency and Computation: Practice and Experience", Volume = 15, Number = 2, Month = feb, Year = 2003, Pages = "117-154", DOI = {10.1002/cpe.713}, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf", Annote = "31 references." } @TechReport{Mueller-Poetzsch-Heffter-Leavens03a, 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, 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://tinyurl.com/q55s5} } @Article{Mueller-Poetzsch-Heffter-Leavens06, Author = {Peter M\"{u}ller and Arnd Poetzsch-Heffter and Gary T. Leavens}, Title = "Modular Invariants for Layered Object Structures", journal = SCP, volume = 62, number = 3, pages = {253-286}, month = oct, year = 2006, URL = {http://dx.doi.org/10.1016/j.scico.2006.03.001} } @TechReport{Raghavan-Leavens05, 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." } @TechReport{Rajan-Leavens07, Author = {Hridesh Rajan and Gary T. Leavens}, Title = {Quantified, Typed Events for Improved Separation of Concerns}, institution = {Iowa State University, Department of Computer Science}, year = 2007, number = {07-14c}, month = oct, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR07-14/TR.pdf", Annote = "37 references." } @TechReport{Rajan-Leavens07a, Author = {Hridesh Rajan and Gary T. Leavens}, Title = {Ptolemy: A Language of Quantified, Typed Events}, institution = {Iowa State University, Department of Computer Science}, year = 2007, number = {07-13a}, month = oct, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR07-13/TR.pdf", Annote = "14 references." } @InCollection{Rodriguez-etal05, 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}, URL = {http://dx.doi.org/10.1007/11531142_24}, annote = {39 references.} } @TechReport{Rodriguez-etal05a, 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 = {Appears in \textit{ECOOP 2005}, LNCS vol 3686, pages 551--576.}, URL = {http://spex.projects.cis.ksu.edu/papers/SAnToS-TR2004-10.pdf} } @InProceedings{Ruby-Leavens00, 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.", doi = {http://doi.acm.org/10.1145/353171.353186} } @TechReport{Ruby-Leavens00a, 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." } @InProceedings{Shaner-Leavens-Naumann07, author = {Steve M. Shaner and Gary T. Leavens and David A. Naumann}, title = {Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs}, booktitle = {International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Montreal, Canada }, pages = {351-367}, year = 2007, month = {oct}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR07-04/TR.pdf}, organization = ACM, annote = {42 references. Grey-box model programs in JML.} } @TechReport{Shaner-Leavens-Naumann07a, author = {Steve M. Shaner and Gary T. Leavens and David A. Naumann}, title = {Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs}, institution = {Iowa State University, Department of Computer Science}, year = 2007, number = {07-04b}, month = {jul}, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR07-04/TR.pdf}, annote = {42 references.}, note = {To appear in OOPSLA 2007.} } @TechReport{Wahls-Baker-Leavens93, 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." } @TechReport{Wahls-Baker-Leavens94, Author = "Tim Wahls and Albert L. Baker and Gary T. Leavens", Title = "The Direct Execution of {SPECS-C++}: A Model-Based Specification Language for {C++} Classes", Institution = "Department of Computer Science, Iowa State University", Year = 1994, Number = "94-02b", Address = "226 Atanasoff Hall, Ames, Iowa 50011", Month = mar, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-02/TR.ps.Z", Annote = "36 references." } @Article{Wahls-Leavens-Baker00, 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, 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, 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, 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, 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" }