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 86 2010-02-10 03:45:25Z gary.leavens $ % 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: 2010-02-09 22:45:25 -0500 (Tue, 09 Feb 2010) $", %%% 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(at)eecs.ucf.edu", %%% dates = {1980--}, %%% keywords = "type, specification, verification, object-oriented", %%% supported = "yes", %%% supported-by = "Gary T. Leavens ", %%% abstract = "Bibliography for Gary T. Leavens" %%% } %%% ==================================================================== @article{Allen-etal08, author = {Eric Allen and Ras Bodik and Kim Bruce and Kathleen Fisher and Stephen Freund and Robert Harper and Chandra Krintz and Shriram Krishnamurthi and Jim Larus and Doug Lea and Gary Leavens and Lori Pollock and Stuart Reges and Martin Rinard and Mark Sheldon and Franklyn Turbak and Mitchell Wand}, editor = {Mark W. Bailey}, title = {SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations}, journal = SIGPLAN, volume = 43, number = 11, year = 2008, month = nov, pages = {6-29}, doi = {http://doi.acm.org/10.1145/1480828.1480831}, publisher = ACM, address = NY } @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." } @InCollection{Boyland-etal08, author = {John Boyland and Dave Clarke and Gary Leavens and Francesco Logozzo and Arnd Poetzsch-Heffter}, title = {Formal Techniques for {Java}-Like Programs}, booktitle = {Object-Oriented Technology ECOOP 2007 Workshop Reader}, pages = {99-107}, publisher = SV, year = 2008, volume = 4906, series = LNCS, address = NY, DOI = {http://dx.doi.org/10.1007/978-3-540-78195-0_10}, annote = {6 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." } @TechReport{Boysen-Leavens08, author = {Kristina P. Boysen and Gary T. Leavens}, title = {Discussion of Design Alternatives for {JML Java 5} Annotations}, institution = "Department of Computer Science, Iowa State University", year = 2008, number = "08-01", address = "226 Atanasoff Hall, Ames, Iowa 50011", month = jan, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR08-01/TR.pdf", Annote = "1 reference." } @article{Bruce-etal00, author = {Kim Bruce and Benjamin Goldberg and Chris Haynes and Gary T. Leavens and John Mitchell}, title = {Proposed knowledge units for programming languages for {Curriculum 2001}}, journal = SIGPLAN, volume = 35, number = 4, year = 2000, month = apr, pages = {29--43}, doi = {http://doi.acm.org/10.1145/346443.346450}, publisher = ACM, address = NY } @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.", URL = {http://doi.acm.org/10.1145/191080.191083} } @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.}, DOI = {http://dx.doi.org/10.1007/3-540-47993-7_10} } @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.", URL = "http://doi.acm.org/10.1145/196092.195325" } @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 = "DOI: 10.1002/spe.649" } @InProceedings{Cheon-etal08, Author = "Yoonsik Cheon and Antonio Cortes and Martine Ceberio and Gary T. Leavens", Title = "Integrating Random Testing with Constraints for Improved Efficiency and Diversity", BookTitle = "Proceedings of SEKE 2008: The 20th International Conference on Software Engineering and Knowledge Engineering", Month = jul, Year = 2008, pages = "861-866", location = "San Francisco, CA", URL = "http://www.cs.utep.edu/~cheon/techreport/tr08-07.pdf" } @TechReport{Cheon-etal08a, Author = "Yoonsik Cheon and Antonio Cortes and Martine Ceberio and Gary T. Leavens", Title = "Integrating Random Testing with Constraints for Improved Efficiency and Diversity", Institution = "Department of Computer Science, The University of Texas at El Paso", Month = may, Year = 2008, Number = "08-07", Note = "In \emph{SEKE 2008}, pages 861-866", URL = "http://www.cs.utep.edu/~cheon/techreport/tr08-07.pdf" } @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.} } @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-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 = "http://doi.acm.org/10.1145/354222.353181", 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} } @InProceedings{Cok-Leavens08, author = {David Cok and Gary T. Leavens}, title = {Extensions of the theory of observational purity and a practical design for {JML}}, booktitle = {Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008)}, pages = {43-50}, year = 2008, number = {CS-TR-08-07}, series = {Technical Report}, address = {4000 Central Florida Blvd., Orlando, Florida, 32816-2362}, organization = {School of EECS, UCF}, annote = {14 references.}, url = {http://www.eecs.ucf.edu/SAVCBS/2008/papers/Cok-Leavens.pdf} } @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}, DOI = {http://dx.doi.org/10.1007/3-540-44555-2_4} } @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}" } @TechReport{Haddad-Leavens08, author = {Ghaith Haddad and Gary T. Leavens}, title = {Extensible Dynamic Analysis for JML: A Case Study with Loop Annotations}, institution = {School of Electrical Engineering and Computer Science, University of Central Florida}, year = 2008, number = {CS-TR-08-05}, address = {Orlando, Florida}, month = {April}, annote = {18 references.} } @TechReport{Hatcliff-etal09, author = {John Hatcliff and Gary T. Leavens and K. Rustan M. Leino and Peter M\"{u}ller and Matthew Parkinson}, title = {Behavioral Interface Specification Languages}, institution = {University of Central Florida, School of EECS}, year = 2009, number = {CS-TR-09-01}, address = {Orlando, FL}, month = mar, url = {\url{http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-09-01/TR.pdf}} } @misc{Hoare-etal07, AUTHOR={Tony Hoare and Gary T. Leavens and Jayadev Misra and Natarajan Shankar}, TITLE={The Verified Software Initiative: A Manifesto}, HOWPUBLISHED={\url{http://qpq.csl.sri.com/vsr/manifesto.pdf}}, YEAR={2007} } @article{Hoare-etal09, address = {New York, NY, USA}, author = {C. A. R. Hoare and Jayadev Misra and Gary T. Leavens and Natarajan Shankar}, issn = {0360-0300}, journal = ACMCS, number = 4, pages = {22:1-22:8}, publisher = ACM, title = {The Verified Software Initiative: A Manifesto}, url = {http://dx.doi.org/10.1145/1592434.1592439}, volume = 41, month = oct, year = 2009 } @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 = "http://dx.doi.org/10.1016/S0096-0551(97)00002-7", 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 = "\url{http://dx.doi.org/10.1007/3-540-48118-4_8}", 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 = 2008, booktitle = {Verified Software: Theories, Tools, Experiments, Zurich, Switzerland}, editor = {Bertrand Meyer and Jim Woodcock}, publisher = SV, volume = 4171, series = LNCS, pages = "134-143", URL = {\url{http://dx.doi.org/10.1007/978-3-540-69149-5_15}}, 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." } @inproceedings{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}, booktitle = {SPLAT '07: Proceedings of the 5th workshop on Engineering properties of languages and aspect technologies}, year = 2007, isbn = {1-59593-656-1}, pages = {1-5}, location = {Vancouver, British Columbia, Canada}, doi = {http://doi.acm.org/10.1145/1233843.1233849}, publisher = ACM, address = NY } @TechReport{Leavens-Clifton07a, 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, doi = {http://dx.doi.org/10.1007/978-3-540-73368-3_6}, 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-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} } @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} } @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.", doi = {http://dx.doi.org/10.1007/s002360050168} } @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.", URL = "\url{http://dx.doi.org/10.1007/3-540-55511-0_7}" } @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 = "http://dx.doi.org/10.1016/S0304-3975(97)87172-1", 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.", URL = {http://dx.doi.org/10.1016/0898-1221(92)90034-F} } @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 SA 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 = "http://doi.acm.org/10.1145/298151.298433", } @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.", URL = "http://doi.acm.org/10.1145/97945.97970" } @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 = "http://dx.doi.org/10.1007/BFb0030623" } @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 = "http://dx.doi.org/10.1007/b14033", 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}} } @Unpublished{Leavens-etal08, 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 and Daniel M. Zimmerman}, Title = {{JML Reference Manual}}, Month = may, Year = 2008, 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} } @TechReport{Leavens07, Author = "Gary T. Leavens", Title = "Following the Grammar", Month = nov, Year = 2007, Institution = "School of EECS, University of Central Florida", Address = "Orlando, FL, 32816-2362", Number = "CS-TR-07-10b", URL = "http://www.eecs.ucf.edu/~leavens/COP4020/docs/follow-grammar.pdf", Annote = "9 references." } @inproceedings{Leavens07a, author = {Gary T. Leavens}, title = {Tutorial on {JML}, the {Java Modeling Language}}, booktitle = {ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering}, year = 2007, pages = 573, location = {Atlanta, Georgia, USA}, doi = {http://doi.acm.org/10.1145/1321631.1321747}, publisher = {ACM}, address = {New York, NY, USA}, } @Article{Leavens08, author = {Gary T. Leavens}, title = {Use Concurrent Programming Models to Motivate Teaching of Programming Languages}, journal = SIGPLAN, volume = 43, number = 11, year = 2008, pages = {93-98}, doi = {http://doi.acm.org/10.1145/1480828.1480849}, publisher = ACM, address = NY, annote = {7 references.} } @TechReport{Leavens08a, author = {Gary T. Leavens}, title = {Use Concurrent Programming Models to Motivate Teaching of Programming Languages}, institution = {School of Electrical Engineering and Computer Science, University of Central Florida}, year = 2008, number = {CS-TR-08-04a}, address = {Orlando, Florida}, month = {May}, annote = {7 references.} } @TechReport{Leavens09, Author = "Gary T. Leavens", Title = "Following the Grammar", Month = oct, Year = 2009, Institution = "School of EECS, University of Central Florida", Address = "Orlando, FL, 32816-2362", Number = "CS-TR-07-10c", URL = "http://www.eecs.ucf.edu/~leavens/COP4020/docs/follow-grammar.pdf", Annote = "9 references." } @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{Leavens94d, author = "Gary T. Leavens", title = "Programs, Recursion and Unbounded Choice by Wim Hesselink", journal = "SIAM Review", year = 1994, volume = 36, number = 1, pages = "131-133", month = mar } @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-etal08, author = {Hridesh Rajan and Jia Tao and Steve M. Shaner and Gary T. Leavens}, title = {Reconciling Trust and Modularity in Web Services}, institution = {Department of Computer Science, Iowa State University}, year = {2008}, number = {08-07}, month = jul, URL = {ftp://ftp.cs.iastate.edu/pub/techreports/TR08-07/TR.pdf}, Annote = {51 references} } @InProceedings{Rajan-etal09, author = {Hridesh Rajan and Jia Tao and Steve M. Shaner and Gary T. Leavens}, title = {Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services}, booktitle = {Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009}, editor = {Giuseppe Castagna}, series = LNCS, volume = 5502, publisher = SV, address = {Berlin}, month = mar, year = 2009 } @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." } @InProceedings{Rajan-Leavens08, author = {Hridesh Rajan and Gary T. Leavens}, title = {Ptolemy: A Language with Quantified, Typed Events}, booktitle = {ECOOP 2008 -- Object-Oriented Programming: 22nd European Conference, Paphos, Cyprus}, pages = {155-179}, year = 2008, editor = {Jan Vitek}, volume = 5142, series = LNCS, address = {Berlin}, month = jul, publisher = SV, URL = {http://dx.doi.org/10.1007/978-3-540-70592-5_8}, annote = {47 references.} } @InProceedings{Rebelo-etal09, author = {Henrique Reb\^{e}lo and Ricardo Lima and M\'{a}rcio Corn\'{e}lio and Gary T. Leavens and Alexandre Mota and C\'{e}sar Oliveira}, title = {Optimizing JML Feature Compilation in Ajmlc Using Aspect-Oriented Refactorings}, booktitle = {XIII Brazilian Symposium on Programming Languages (SBLP)}, publisher = {Brazilian Computer Society}, year = 2009, month = aug, annote = {25 references.}, pages = {117-130} url = {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-09-05/TR.pdf} } @TechReport{Rebelo-etal09a, author = {Henrique Reb\^{e}lo and Ricardo Lima and M\'{a}rcio Corn\'{e}lio and Gary T. Leavens and Alexandre Mota and C\'{e}sar Oliveira}, title = {Optimizing JML Features Compilation in Ajmlc Using Aspect-Oriented Refactorings}, number = {CS-TR-09-05}, series = {Technical Report}, address = {4000 Central Florida Blvd., Orlando, Florida, 32816-2362}, organization = {School of EECS, UCF}, year = 2009, month = apr, annote = {30 references.}, note = {To appear in SBLP'09.}, url = {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-09-05/TR.pdf} } @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", publisher = ACM, address = NY, 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}, doi = {http://doi.acm.org/10.1145/1297027.1297053}, 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.} } @InProceedings{Shaner-Rajan-Leavens08, author = {Steve Shaner and Hridesh Rajan and Gary T. Leavens}, title = {Model Programs for Preserving Composite Invariants}, booktitle = {Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008)}, pages = {95-100}, year = 2008, number = {CS-TR-08-07}, series = {Technical Report}, address = {4000 Central Florida Blvd., Orlando, Florida, 32816-2362}, organization = {School of EECS, UCF}, annote = {16 references.}, url = {http://www.eecs.ucf.edu/SAVCBS/2008/papers/Shaner-Rajan-Leavens.pdf} } @TechReport{Taylor-Rieken-Leavens08, author = {Kristina B. Taylor and Johannes Rieken and Gary T. Leavens}, title = {Adapting the {Java Modeling Language (JML)} for {Java 5} Annotations}, institution = "Department of Computer Science, Iowa State University", year = 2008, number = "08-06", address = "226 Atanasoff Hall, Ames, Iowa 50011", month = apr, URL = "ftp://ftp.cs.iastate.edu/pub/techreports/TR08-06/TR.pdf", Annote = "13 references." } @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 = "http://dx.doi.org/10.1023/A:1026554217992" } @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, URL = {http://doi.acm.org/10.1145/372202.372465} } @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" }