% $Id$
% 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$",
%%%     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
}

@inproceedings{Aotani-Leavens16,
 author = {Tomoyuki Aotani and Gary T. Leavens},
 title = {Towards Modular Reasoning for Context-Oriented Programs},
 booktitle = {Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs},
 series = {FTfJP'16},
 year = {2016},
 location = {Rome, Italy},
 pages = {8:1--8:7},
 articleno = {8},
 numpages = {7},
 url = {http://doi.acm.org/10.1145/2955811.2955819},
 doi = {10.1145/2955811.2955819},
 publisher = {ACM},
 address = NY,
 annote = "15 references."
} 

@TechReport{Assaad-Leavens01,
  author =	 {Medhat G. Assaad and Gary T. Leavens},
  title =	 {Alias-free parameters in {C} for Better Reasoning
                  and Optimization},
  institution =	 "Department of Computer Science, Iowa State
                  University",
  year =	 2001,
  number =	 "01-11",
  address =	 "226 Atanasoff Hall, Ames, Iowa 50011",
  month =	 nov,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR01-11/TR.pdf",
  Note =	 "Available from archives.cs.iastate.edu.",
  Annote =	 "Applies the ACL approach to C. Describes the
                  optimization opportunities that arise. 33
                  references."
}
            
@TechReport{Bagherzadeh-etal10,
Author = {Mehdi Bagherzadeh and Hridesh Rajan and Gary T. Leavens and Sean Mooney},
Title = {Translucid Contracts: Expressive Specification and Modular Verification for Aspect-oriented Interfaces},
institution = {Department of Computer Science, Iowa State University},
year = 2010,
number = {10-02a},
month = jul,
URL = {http://www.cs.iastate.edu/~design/papers/TR-10-02/TR-10-02.pdf},
Annote = {32 references.}                  
}

@InProceedings{Bagherzadeh-etal10a,
Author = {Mehdi Bagherzadeh and Hridesh Rajan and Gary T. Leavens and Sean Mooney},
Title = {Translucid Contracts for Modular Reasoning about Aspect-oriented Programs},
BookTitle = {SPLASH'10 Companion},
year = 2010,
pages = {245-246},
month = oct,
URL = {http://dx.doi.org/10.1145/1869542.1869596},
Annote = {7 references.}                  
}

@InProceedings{Bagherzadeh-etal11,
 Author = {Mehdi Bagherzadeh and Hridesh Rajan and Gary T. Leavens and Sean Mooney},
 Title = {Translucid Contracts: Expressive Specification and Modular Verification for Aspect-oriented Interfaces},
 booktitle = {Proceedings of the tenth international conference on Aspect-oriented software development},
 series = {AOSD '11},
 month = mar,
 year = {2011},
 location = {Porto de Galinhas, Brazil},
 pages = {141--152},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1960275.1960293},
 doi = {http://doi.acm.org/10.1145/1960275.1960293},
 acmid = {1960293},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{Bagherzadeh-Leavens-Dyer11,
 author = {Mehdi Bagherzadeh and Gary T. Leavens and Robert Dyer},
 title = {Applying translucid contracts for modular reasoning about aspect and object oriented events},
 booktitle = {Proceedings of the 10th international workshop on Foundations of aspect-oriented languages},
 series = {FOAL '11},
 year = {2011},
 location = {Porto de Galinhas, Brazil},
 pages = {31--35},
 numpages = {5},
 url = {http://doi.acm.org/10.1145/1960510.1960517},
 doi = {http://doi.acm.org/10.1145/1960510.1960517},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@InBook{Bao-Leavens18,
  author = 	 {Yuyan Bao and Gary T. Leavens},
  title = 	 {Principled Software Development: Essays Dedicated to
                  {Arnd Poetzsch-Heffter} on the Occasion of his 60th Birthday},
  chapter = 	 {A Methodology for Invariants, Framing, and Subtyping in {JML}},
  publisher = 	 SV,
  year = 	 2018,
  address = 	 {Switzerland},
  pages = 	 {19-39},
  annote = 	 {32 references.}
}

@TechReport{Bao-Leavens-Ernst14,
  author = 	 {Yuyan Bao and Gary T. Leavens and Gidon Ernst},
  title = 	 {Translating Separation Logic into Dynamic Frames Using Fine-Grained Region Logic},
  institution =  {Computer Science, University of Central Florida},
  year = 	 2014,
  number = 	 {CS-TR-13-02a},
  address = 	 {Orlando, Florida},
  month = 	 mar,
  URL =         {\url{http://goo.gl/jLv7g0}},
  Note =         {\url{http://goo.gl/jLv7g0}},
  annote =      {21 references.}
}

@TechReport{Bao-Leavens-Ernst15,
  author = 	 {Yuyan Bao and Gary T. Leavens and Gidon Ernst},
  title = 	 {Conditional Effects in Fine-grained Region Logic},
  institution =  {Computer Science, University of Central Florida},
  year = 	 2015,
  number = 	 {CS-TR-15-01},
  address = 	 {Orlando, Florida},
  month = 	 mar,
  annote = 	 {13 references.}
}

@inproceedings{Bao-Leavens-Ernst15a,
  author = {Yuyan Bao and Gary T. Leavens and Gidon Ernst},
  title = {Conditional Effects in Fine-grained Region Logic},
  booktitle = {Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs},
  series = {FTfJP '15},
  year = {2015},
  isbn = {978-1-4503-3656-7},
  location = {Prague, Czech Republic},
  pages = {5:1--5:6},
  articleno = {5},
  numpages = {6},
  url = {http://doi.acm.org/10.1145/2786536.2786537},
  doi = {10.1145/2786536.2786537},
  acmid = {2786537},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {formal specification, formal verification, framing, hoare logic, region logic}
}

@article{Bao-Leavens-Ernst18,
  author = {Yuyan Bao and Gary T. Leavens and Gidon Ernst},
  year = 2018,
  title = {Unifying separation logic and region logic to allow interoperability},
  journal = {Formal Aspects of Computing},
  issn = {0934-5043},
  doi = {10.1007/s00165-018-0455-5},
  volume = 30,
  month = 5,
  pages = {381–441},
  url = {http:https://doi.org/10.1007/s00165-018-0455-5},
  abstract = {Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.},
  annote = {61 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."
}

% DOI = {10.1007/11804192_16},
@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 =          {https://tinyurl.com/4tk2nzzd}
}

@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."
}

% DOI = {10.1007/3-540-44555-2_4},
@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.},
  URL = {https://tinyurl.com/kn954nm8}
}

@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.}
}

@TechReport{Elva-Leavens12,
  author = 	 {Rochelle Elva and Gary T. Leavens},
  title = 	 {{JSCTracker}: A Semantic Clone Detection Tool for {Java} Code},
  institution =  {Computer Science, University of Central Florida},
  year = 	 2012,
  number = 	 {CS-TR-12-04},
  address = 	 {Orlando, Florida},
  month = 	 mar,
  annote = 	 {27 references.}
}

@InProceedings{Elva-Leavens12a,
  author = 	 {Rochelle Elva and Gary T. Leavens},
  title = 	 {Semantic Clone Detection using method {IOE}-behavior},
  booktitle = {6th International Workshop on Software Clones (IWSC), Zurich},
  year = 	 2012,
  pages = 	 {80-81},
  month = 	 jun,
  publisher = IEEE,
  URL = {http://dx.doi.org/10.1109/IWSC.2012.6227874},
  annote = 	 {8 references.}
}

@TechReport{Elva-Leavens12b,
  author = 	 {Rochelle Elva and Gary T. Leavens},
  title = 	 {{JSCTracker}: JSCTracker: A Tool and Algorithm for Semantic Method Clone Detection Using Method IOE-Behavior},
  institution =  {Computer Science, University of Central Florida},
  year = 	 2012,
  number = 	 {CS-TR-12-07},
  address = 	 {Orlando, Florida},
  month = 	 oct,
  annote = 	 {11 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},
  URL = {http://http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-08-05/TR.pdf},
  annote = 	 {18 references.}
}
                  
@TechReport{Haddad-Leavens11,
  author = 	 {Ghaith Haddad and Gary T. Leavens},
  title = 	 {Specifying Subtypes in {SCJ} Programs},
  institution =  {Dept.\ of Electrical Engineering and Computer Science, University of Central Florida},
  year = 	 2011,
  number = 	 {CS-TR-11-04},
  address = 	 {Orlando, Florida},
  month = 	 {July},
  URL =          {http://http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-11-04/TR.pdf},
  annote = 	 {35 references.}
}
                  
@article {Haddad-Leavens13,
author = {Ghaith Haddad and Gary T. Leavens},
title = {Specifying subtypes in {Safety Critical Java} programs},
journal = {Concurrency and Computation: Practice and Experience},
publisher = {John Wiley \& Sons, Ltd},
url = {http://dx.doi.org/10.1002/cpe.2930},
doi = {10.1002/cpe.2930},
volume=25,
number=16,
pages = {2290-2306},
keywords = {SafeJML, Safety Critical Java (SCJ), Java Modeling Language (JML), timing behavior, duration, performance, WCET},
month = nov,
year = 2013,
}

@TechReport{Haddad-Hussain-Leavens10a,
  author = 	 {Ghaith Haddad and Faraz Hussain and Gary T. Leavens},
  title = 	 {The Design of {SafeJML}, a Specification Language for {SCJ} with Support for {WCET} Specification},
  institution =  {School of Electrical Engineering and Computer Science, 
University of Central Florida},
  year = 	 2010,
  number = 	 {CS-TR-10-06},
  address = 	 {Orlando, Florida},
  month = 	 jun,
  annote = 	 {38 references.}
}

@inproceedings{Haddad-Hussain-Leavens10b,
 author = {Haddad, Ghaith and Hussain, Faraz and Leavens, Gary T.},
 title = {The design of {SafeJML}, a specification language for {SCJ} with support for {WCET} specification},
 booktitle = {Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems},
 series = {JTRES '10},
 year = {2010},
 isbn = {978-1-4503-0122-0},
 location = {Prague, Czech Republic},
 pages = {155--163},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/1850771.1850793},
 doi = {http://doi.acm.org/10.1145/1850771.1850793},
 acmid = {1850793},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {SafeJML, WCET, duration, java modeling language (JML), performance, safety critical Java (SCJ), timing behavior},
} 

@InProceedings{Hussain-Leavens10,
	author={Faraz Hussain and Gary T. Leavens},
	booktitle={2010 8th IEEE International Conference on Software Engineering and Formal Methods}, 
	title={temporaljmlc: A {JML} Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties}, 
	year=2010,
	pages={63-72},
	publisher=IEEE,
	address="Los Altos",
	doi={10.1109/SEFM.2010.15}
}

@TechReport{Hussain-Leavens10a,
  author = 	 {Faraz Hussain and Gary T. Leavens},
  title = 	 {temporaljmlc: A {JML} Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties},
  institution =  {UCF, Dept. of EECS},
  year = 	 2010,
  number = 	 {CS-TR-10-08},
  address = 	 {Orlando, Florida},
  month = 	 {jul},
  annote = 	 {25 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}}
}

@TechReport{Hatcliff-etal10,
  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 = 	 2010,
  number = 	 {CS-TR-09-01a},
  address = 	 {Orlando, FL},
  month = 	 oct,
  url = {\url{http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-09-01/TR.pdf}}
}

@Article{Hatcliff-etal12,
 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},
 journal =      ACMCS,
 volume = 44,
 number = 3,
 month = jun,
 year = 2012,
 pages = {16:1--16:58},
 url = {http://doi.acm.org/10.1145/2187671.2187678},
 doi = {10.1145/2187671.2187678},
 publisher = ACM,
 address = NY
} 

@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."
}

@Article{Khairunnesa-etal23,
  author = 	 {Samantha Syeda Khairunnesa and Shibbir Ahmed and Sayem Mohammad Imtiaz and Hridesh Rajan and Gary T. Leavens},
  title = 	 {What kinds of contracts do {ML} {APIs} need?},
  journal = 	 {Empirical Software Engineering},
  year = 	 2023,
  URL = {https://doi.org/10.1007/s10664-023-10320-z},
  volume = 	 28,
  number = 	 6,
  pages = 	 {142-179}
}


@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}
}

@incollection{Klebanov-etal11,
author={Vladimir Klebanov and Peter M\"{u}ller and Natarajan Shankar and Gary T. Leavens and Valentin W\"{u}stholz and Eyad Alkassar and Rob Arthan and Derek Bronish and Rod Chapman and Ernie Cohen and Mark Hillebrand and Bart Jacobs and K .Rustan M. Leino and Rosemary Monahan and Frank Piessens and Nadia Polikarpova and Tom Ridge and Jan Smans and Stephan Tobies and Thomas Tuerk and Mattias Ulbrich and Benjamin Weiss},
year={2011},
isbn={978-3-642-21436-3},
booktitle={FM 2011: Formal Methods},
volume={6664},
series=LNCS,
editor={Michael Butler and Wolfram Schulte},
title={The 1st Verified Software Competition: Experience Report},
url={http://dx.doi.org/10.1007/978-3-642-21437-0_14},
publisher={Springer Berlin Heidelberg},
pages={154-168},
annote={14 references}
}

@TechReport{Kulczycki-etal02,
  Author =	 {Gregory W. Kulczycki and Murali Sitaraman and
                  William F. Ogden and Bruce W. Weide and Gary
                  T. Leavens},
  Title =	 "Reasoning about Procedure Calls with Repeated
                  Arguments and the Reference-Value Distinction",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Address =	 "Ames, Iowa, 50011",
  Number =	 "02-13",
  Year =	 2002,
  Month =	 dec,
  Annote =	 "Call by swapping compared with other mechanisms. 50
                  references."
}

@TechReport{Kulczycki-etal03,
  Author =	 {Gregory W. Kulczycki and Murali Sitaraman and
                  William F. Ogden and Gary T. Leavens},
  Title =	 "Reasoning about Procedure Calls with Repeated
                  Arguments and the Reference-Value Distinction",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Address =	 "Ames, Iowa, 50011",
  Number =	 "02-13a",
  Year =	 2003,
  Month =	 dec,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-13/TR.pdf",
  Annote =	 "Three approaches to avoiding aliasing due to
                  repeated arguments. 63 references."
}

@TechReport{Leavens-Antropova99,
  Author =	 "Gary T. Leavens and Olga Antropova",
  Title =	 "{ACL} --- Eliminating Parameter Aliasing with
                  Dynamic Dispatch",
  Year =	 1999,
  Month =	 feb,
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Address =	 "Ames, Iowa, 50011",
  Number =	 "98-08a",
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-08/TR.ps.gz",
  Note =	 "Available by anonymous ftp from ftp.cs.iastate.edu,
                  and by e-mail from almanac@cs.iastate.edu"
}

@Article{Leavens-Baker-Ruby06,
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "Preliminary Design of {JML}: A Behavioral Interface Specification Language for {Java}",
  journal = SIGSOFT,
  volume = 31,
  number = 3,
  month = mar,
  year = 2006,
  pages = {1-38},
  URL = {\url{http://doi.acm.org/10.1145/1127878.1127884}},
  publisher = ACM,
  address = NY
}

@TechReport{Leavens-Baker-Ruby06a,
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "Preliminary Design of {JML}: A Behavioral Interface
                  Specification Language for {Java}",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Year =	 2006,
  Number =	 "98-06-rev29",
  Month =	 jan,
  URL =          "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.pdf",
  Annote =	 "79 references.",
  Note =	 "Also \emph{ACM SIGSOFT Software Engineering Notes}, 31(3):1-38, March 2006."
}

@InProceedings{Leavens-Baker-Ruby98,
  author =	 {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
  title =	 {{JML}: a {Java Modeling Language}},
  booktitle =	 {Formal Underpinnings of Java Workshop (at OOPSLA
                  '98)},
  year =	 1998,
  month =	 oct,
  note =	 {{\tt
                  http://www-dse.doc.ic.ac.uk/{\char'176}sue/oopsla/cfp.html}}
}

@InCollection{Leavens-Baker-Ruby99b,
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "{JML}: A Notation for Detailed Design",
  BookTitle =	 "Behavioral Specifications of Businesses and Systems",
  Editor =	 "Haim Kilov and Bernhard Rumpe and Ian Simmonds",
  Year =	 1999,
  Publisher =	 "Kluwer Academic Publishers",
  Address =	 "Boston",
  Pages =	 "175-188",
  Annote =	 "36 references."
}

@InProceedings{Leavens-Baker99,
  Author =	 "Gary T. Leavens and Albert L. Baker",
  Title =	 "Enhancing the Pre- and Postcondition Technique for
                  More Expressive Specifications",
  Editor =	 "Jeannette M. Wing and Jim Woodcock and Jim Davies",
  BookTitle =	 "FM'99 --- Formal Methods: World Congress on Formal
                  Methods in the Development of Computing Systems,
                  Toulouse, France, September 1999, Proceedings",
  Year =	 1999,
  Series =	 LNCS,
  Publisher =	 "Springer-Verlag",
  Volume =	 1709,
  Pages =	 "1087--1106",
  URL =          "http://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 =          "http://www.jmlspecs.org/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."
}

% DOI = {10.1007/978-3-540-69149-5_15},
@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 = 	 {https://tinyurl.com/5rckhcep},
  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}
}

@TechReport{Leavens-Naumann13,
  author = 	 {Gary T. Leavens and David A. Naumann},
  title = 	 {Behavioral Subtyping, Specification Inheritance, and Modular Reasoning},
  Institution =	 "Computer Science, University of Central Florida",
  Address =	 "Orlando, FL, 32816",
  Number =	 "CS-TR-13-03",
  year = 	 2013,
  month =	 jun,
  annote =	 {81 references.},
  URL =          {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-13-03/TR.pdf}
}

@article{Leavens-Naumann15,
 author = {Gary T. Leavens and David A. Naumann},
 title = {Behavioral Subtyping, Specification Inheritance, and Modular Reasoning},
 journal = {TOPLAS},
 volume = 37,
 number = 4,
 month = aug,
 year = 2015,
 pages = {13:1--13:88},
 articleno = 13,
 numpages = 88,
 url = {http://doi.acm.org/10.1145/2766446},
 doi = {10.1145/2766446},
 publisher = {ACM},
 address = NY,
 annotate = {85 references.}
}

@InProceedings{Leavens-Naumann18,
author="Gary T. Leavens and David A. Naumann",
editor="Jonathan P. Bowen and Zhiming Liu and Zili Zhang",
title="An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping",
booktitle="Engineering Trustworthy Software Systems",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="39--88",
isbn="978-3-030-02928-9"
}

@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}}
}

@Inbook{Leavens-etal16,
author="Gary T. Leavens and David Naumann and Hridesh Rajan and Tomoyuki Aotani",
editor="Tiziana Margaria and Bernhard Steffen",
title="Specifying and Verifying Advanced Control Features",
bookTitle="Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II",
year="2016",
publisher=Springer,
address="Cham",
pages="80--96",
doi="10.1007/978-3-319-47169-3_7",
url="http://dx.doi.org/10.1007/978-3-319-47169-3_7"
}

@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."
}

@InProceedings{Leavens10,
  author = 	 {Gary T. Leavens},
  title = 	 {The Future of Library Specification},
  booktitle = {Future of Software Engineering Research Workshop},
  year = 	 2010,
  month = 	 nov,
  organization = ACM,
  note =         {To appear.}
}

@TechReport{Leavens10a,
  author = 	 {Gary T. Leavens},
  title = 	 {The Future of Library Specification},
  institution =  {Dept. of EECS, University of Central Florida},
  year = 	 2010,
  number = 	 {CS-TR-10-09},
  Address =	 "Orlando, FL, 32816-2362",
  month = 	 aug,
  URL =          "http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-10-09/TR.pdf",
  annote = 	 {19 references.}
}
                  
@TechReport{Leavens13,
  Author =	 "Gary T. Leavens",
  Title =	 "Following the Grammar with {Haskell}",
  Month =	 jan,
  Year =	 2013,
  Institution =	 "Dept. of EECS, University of Central Florida",
  Address =	 "Orlando, FL, 32816-2362",
  Number =	 "CS-TR-13-01",
  URL =          "http://www.eecs.ucf.edu/~leavens/COP4020/docs/follow-grammar-haskell.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}
}

@InProceedings{Nilzadeh-etal17,
  author = 	 {Amirfarhad Nilzadeh and Wojciech Mazurczyk and Cliff Zou and Gary T. Leavens},
  title = 	 {Information Hiding in {RGB} Images Using an Improved Matrix Pattern Approach},
  booktitle = {The First International Workshop on The Bright and Dark Sides of Computer Vision: Challenges and Opportunities for Privacy and Security (CV-COPS 2017)},
  year = 	 2017,
  month = 	 jul,
  publisher =    IEEE,
  annote =       {34 references.},
  DOI = {https://doi.org/10.1109/CVPRW.2017.183},
  URL={\url{http://openaccess.thecvf.com/content_cvpr_2017_workshops/w16/papers/Leavens_Information_Hiding_in_CVPR_2017_paper.pdf}}
}

@INPROCEEDINGS{Nilizadeh-etal21ce,
  author={Amirfarhad Nilizadeh and Marlon Calvo and Gary T. Leavens and Xuan-Bach D. Le},
  booktitle={2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)}, 
  title={More Reliable Test Suites for Dynamic APR by using Counterexamples}, 
  year={2021},
  pages={208-219},
  publisher={IEEE},
  address="Los Altos",
  doi={10.1109/ISSRE52982.2021.00032},
  annote="95 references."
}

% doi={10.1109/ICST49551.2021.00033},
@InProceedings{Nilizadeh-etal21exploring,
  author={Amirfarhad Nilizadeh and Gary T. Leavens and Xuan-Bach D. Le and Corina S. P{\u{a}}s{\u{a}}reanu and David R. Cok},
  booktitle={2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)}, 
  title={Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods}, 
  year={2021},
  pages={229-240},
  url = {https://tinyurl.com/bn3ecw98},
  annotate={84 references.}
}

% DOI={10.1007/978-3-030-79379-1_5},
@InProceedings{Nilizadeh-Leavens-Pasareanu21,
author="Amirfarhad Nilizadeh and Gary T. Leavens and Corina S. P{\u{a}}s{\u{a}}reanu",
editor={Fr{\'e}d{\'e}ric Loulergue and Franz Wotawa},
title="Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs",
booktitle="Tests and Proofs",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="72-84",
url = {https://tinyurl.com/4xzxxrn2},
abstract="Software is widely used in critical systems. Thus, it is important that developers can quickly find semantic bugs with testing; however, semantic bugs can only be revealed by tests that use valid inputs. Guided fuzzers can create input tests that cover all branches; however, they may not necessarily cover all branches with valid inputs. Therefore, the problem is how to guide a fuzzer to cover all branches in a program with only valid inputs. We perform a study of an idea that guarantees that all inputs generated by a guided fuzzer that reach the program under test are valid using formal specifications and runtime assertion checking. Our results show that this idea improves the feedback given to a guided fuzzer.",
isbn="978-3-030-79379-1"
}

@article{Nilizadeh-etal22,
  author={Amirfarhad Nilizadeh and Shirin Nilizadeh and Wojciech Mazurczyk and Cliff Zou and Gary T. Leavens},
  title={Adaptive Matrix Pattern Steganography on {RGB} Images},
  journal={Journal of Cyber Security and Mobility},
  year=2022,
  volume=11,
  number=1,
  pages={1-28},
  publisher=Elsevier,
  annote="83 references."
}

@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,
  pages={333-347},
  url={http://dx.doi.org/10.1007/978-3-642-00590-9_24}
}
                  
@inproceedings{Rajan-etal11,
 author = {Hridesh Rajan and Gary T. Leavens and Robert Dyer and Mehdi Bagherzadeh},
 title = {Modularizing crosscutting concerns with Ptolemy},
 booktitle = {Proceedings of the tenth international conference on Aspect-oriented software development companion},
 series = {AOSD '11},
 year = {2011},
 isbn = {978-1-4503-0606-5},
 location = {Porto de Galinhas, Brazil},
 pages = {61--62},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/1960314.1960332},
 doi = {http://doi.acm.org/10.1145/1960314.1960332},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{Rajan-etal15,
author = {Hridesh Rajan and Tien N. Nguyen and Gary T. Leavens and Robert Dyer},
title = {Inferring Behavioral Specifications from Large-scale Repositories by Leveraging Collective Intelligence}, 
booktitle = {ICSE'15: The 37th International Conference on Software Engineering: NIER Track},
location = {Florence, Italy},
month = {May},
year = {2015},
pages = {579-582},
doi = {http://dx.doi.org/10.1109/ICSE.2015.339}
}

@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}
}

@TechReport{Rebelo-etal11,
  author = 	 {Henrique Reb\^{e}lo and Roberta Coelho and Ricardo Lima and Gary T. Leavens and Alexandre Mota and Fernando Castor},
  title = 	 {On the Interplay of Exception Handling and Design by Contract: An Aspect-Oriented Recovery Approach},
  number = 	 {CS-TR-11-02},
  series = 	 {Technical Report},
  address = 	 {4000 Central Florida Blvd., Orlando, Florida, 32816-2362},
  organization = {Dept. of EECS, UCF},
  year = 	 2011,
  month = 	 apr,
  annote = 	 {21 references.},
  url =          {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-11-02/TR.pdf}
}

@InProceedings{Rebelo-etal14,
 author = {Henrique Reb\^{e}lo and Gary T. Leavens and Mehdi Bagherzadeh and Hridesh Rajan and Ricardo Lima and Daniel M. Zimmerman and M\'{a}rcio Corn{\'e}lio and Thomas Th\"{u}m},
 title = {AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts},
 booktitle = {Proceedings of the 13th International Conference on Modularity},
 series = {MODULARITY '14},
 year = {2014},
 isbn = {978-1-4503-2772-5},
 location = {Lugano, Switzerland},
 pages = {157--168},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2577080.2577084},
 doi = {10.1145/2577080.2577084},
 acmid = {2577084},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {aspect-oriented programming, aspectj, aspectjml, crosscutting contracts, design by contract, jml},
} 

@InProceedings{Rebelo-etal14a,
 author = {Henrique Reb\^{e}lo and Gary T. Leavens and Mehdi Bagherzadeh and Hridesh Rajan and Ricardo Lima and Daniel M. Zimmerman and M\'{a}rcio Corn{\'e}lio and Thomas Th\"{u}m},
 title = {Modularizing Crosscutting Contracts with AspectJML},
 booktitle = {Proceedings of the 13th International Conference on Modularity},
 series = {MODULARITY '14},
 year = {2014},
 isbn = {978-1-4503-2772-5},
 location = {Lugano, Switzerland},
 pages = {21--24},
 numpages = {4},
 url = {http://doi.acm.org/10.1145/2584469.2584476},
 doi = {10.1145/2584469.2584476},
 acmid = {2584476},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {aspect-oriented programming, aspectj, aspectjml, crosscutting contracts, design by contract, jml},
} 

@inproceedings{Rebelo-etal11a,
 author = {Henrique Reb\^{e}lo and Roberta Coelho and Ricardo Lima and Gary T. Leavens and Marieke Huisman and Alexandre Mota and Fernando Castor},
 title = {On the interplay of exception handling and design by contract: an aspect-oriented recovery approach},
 booktitle = {Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs},
 series = {FTfJP '11},
 year = {2011},
 isbn = {978-1-4503-0893-9},
 location = {Lancaster, United Kingdom},
 pages = {7:1--7:6},
 articleno = {7},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2076674.2076681},
 doi = {10.1145/2076674.2076681},
 acmid = {2076681},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@Article{Rebelo-etal13,
  author = 	 {Henrique Reb\^{e}lo and Ricardo Lima and Gary T. Leavens and M\'{a}rcio Corn\'{e}lio and Alexandre Mota and Cesar Oliveira},
  title = 	 {Optimizing generated aspect-oriented assertion checking code for {JML} using program transformations: An empirical study},
  journal = 	 SCP,
  year = 	 2013,
  volume = 	 78,
  number = 	 8,
  pages = 	 {1137-1156},
  month = 	 aug,
  URL = 	 {http://dx.doi.org/10.1016/j.scico.2012.09.003}
}

@inproceedings{Rebelo-etal13a,
 author = {Henrique Rebelo and Gary T. Leavens and Ricardo Massa Ferreira Lima and Paulo Borba and M\'{a}rcio Ribeiro},
 title = {Modular Aspect-oriented Design Rule Enforcement with XPIDRs},
 booktitle = {Proceedings of the 12th Workshop on Foundations of Aspect-oriented Languages},
 series = {FOAL '13},
 year = {2013},
 isbn = {978-1-4503-1865-5},
 location = {Fukuoka, Japan},
 pages = {13--18},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2451598.2451603},
 doi = {10.1145/2451598.2451603},
 acmid = {2451603},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {AspectJ language, JML language, aspect-oriented programming, design rules, runtime assertion checking},
 annote = {19 references.}
} 

@TechReport{Rebelo-Lima-Leavens11,
  author = 	 {Henrique Reb\^{e}lo and Ricardo Lima and Gary T. Leavens},
  title = 	 {Modular Contracts with Procedures, Annotations, Pointcuts and Advice},
  number = 	 {CS-TR-11-05},
  series = 	 {Technical Report},
  address = 	 {4000 Central Florida Blvd., Orlando, Florida, 32816-2362},
  organization = {Dept. of EECS, UCF},
  year = 	 2011,
  month = 	 sep,
  annote = 	 {24 references.},
  note =         {To appear in SBLP'11.},
  url =          {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-11-05/TR.pdf}
}

@TechReport{Rebelo-Leavens-Lima11,
  author = 	 {Henrique Reb\^{e}lo Gary T. Leavens and Ricardo Lima},
  title = 	 {Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking},
  number = 	 {CS-TR-11-07a},
  series = 	 {Technical Report},
  address = 	 {4000 Central Florida Blvd., Orlando, Florida, 32816-2362},
  organization = {Dept. of EECS, UCF},
  year = 	 2011,
  month = 	 dec,
  annote = 	 {32 references.},
  url =          {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-11-07/TR.pdf}
}
    
@TechReport{Rebelo-Leavens-Lima12,
  author = 	 {Henrique Reb\^{e}lo Gary T. Leavens and Ricardo Lima},
  title = 	 {Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking},
  number = 	 {CS-TR-12-03},
  series = 	 {Technical Report},
  address = 	 {4000 Central Florida Blvd., Orlando, Florida, 32816-2362},
  organization = {Dept. of EECS, UCF},
  year = 	 2012,
  month = 	 jan,
  annote = 	 {32 references.},
  url =          {http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-12-03/TR.pdf}
}

@inproceedings{Rebelo-Leavens-Lima13,
 author = {Henrique Reb\^{e}lo and Gary T. Leavens and Ricardo Massa Lima},
 title = {Client-aware Checking and Information Hiding in Interface Specifications with {JML/Ajmlc}},
 booktitle = {Proceedings of the 2013 Companion Publication for Conference on Systems, Programming, \& Applications: Software for Humanity},
 series = {SPLASH '13},
 year = {2013},
 isbn = {978-1-4503-1995-9},
 location = {Indianapolis, Indiana, USA},
 pages = {11--12},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/2508075.2514569},
 doi = {10.1145/2508075.2514569},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {design by contract, information hiding, interface specification languages, java modeling language (JML), runtime assertion checking},
}

@inproceedings{Rebelo-Leavens15,
 author = {Henrique Reb\^{e}lo and Gary T. Leavens},
 title = {Enforcing Information Hiding in Interface Specifications: A Client-aware Checking Approach},
 booktitle = {Companion Proceedings of the 14th International Conference on Modularity},
 series = {MODULARITY Companion 2015},
 year = {2015},
 location = {Fort Collins, CO, USA},
 pages = {47--51},
 numpages = {5},
 url = {http://doi.acm.org/10.1145/2735386.2736750},
 doi = {10.1145/2735386.2736750},
 acmid = {2736750},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {AspectJML language, Information hiding, JML language, interface specification languages, runtime assertion checking},
}

@inproceedings{Rebelo-Leavens17,
 author = {Henrique Reb\^{e}lo and Gary T. Leavens},
 title = {Aspect-Oriented Programming Reloaded},
 booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages},
 series = {SBLP 2017},
 year = 2017,
 isbn = {978-1-4503-5389-2},
 location = {Fortaleza, CE, Brazil},
 pages = {10:1--10:8},
 articleno = 10,
 numpages = 8,
 url = {http://doi.acm.org/10.1145/3125374.3125383},
 doi = {10.1145/3125374.3125383},
 acmid = 3125383,
 publisher = ACM,
 address = {New York, NY, USA},
 keywords = {Aspect-oriented programming, AspectJ, AspectJML, modularity},
} 
            
@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."
}

@InCollection{Sanchez-Leavens13,
author={Jos\'{e} S\'{a}nchez and Gary T. Leavens},
title={Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification},
year={2013},
isbn={978-3-642-39613-7},
booktitle={Software Composition},
volume={8088},
series={Lecture Notes in Computer Science},
editor={Walter Binder and Eric Bodden and Welf L\"{o}we},
doi={10.1007/978-3-642-39614-4_5},
url={http://dx.doi.org/10.1007/978-3-642-39614-4_5},
publisher={Springer-Verlag},
address={Berlin},
pages={65-80}
}

@inproceedings{Sanchez-Leavens14,
 author = {Jos{\'e} S\'{a}nchez and Gary T. Leavens},
 title = {Static Verification of {PtolemyRely} Programs Using {OpenJML}},
 booktitle = {Proceedings of the 13th Workshop on Foundations of Aspect-oriented Languages},
 series = {FOAL '14},
 year = {2014},
 isbn = {978-1-4503-2798-5},
 location = {Lugano, Switzerland},
 pages = {13-18},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2588548.2588550},
 doi = {10.1145/2588548.2588550},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {openjml, ptolemy language, ptolemyrely, static verification},
 annote = {14 references.}
} 

@inproceedings{Sanchez-Leavens16,
 author = {Jos{\'e} S\'{a}nchez and Gary T. Leavens},
 title = {Reasoning Tradeoffs in Languages with Enhanced Modularity Features},
 booktitle = {Proceedings of the 15th International Conference on Modularity},
 series = {MODULARITY 2016},
 year = {2016},
 isbn = {978-1-4503-3995-7},
 location = {Malaga, Spain},
 pages = {13--24},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2889443.2889447},
 doi = {10.1145/2889443.2889447},
 acmid = {2889447},
 publisher = {ACM},
 address = NY,
 keywords = {Modular Verification, Reasoning Tradeoffs},
 annote = {37 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 = 	 {http://doi.acm.org/10.1145/1297027.1297053},
  doi = 	 {http://doi.acm.org/10.1145/1297027.1297053},
  organization = ACM,
  address = NY,
  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}
}

@InProceedings{Singleton-etal18,
  author = 	 {John L. Singleton and Gary T. Leavens and Hridesh Rajan and David Cok},
  title = 	 {Poster: An Algorithm and Tool to Infer Practical Postconditions},
  booktitle = {2018 ACM/IEEE 40th International Conference on Software Engineering: Companion Proceedings},
  year = 	 2018,
  pages = 	 {313-314},
  month = 	 {Jun},
  address = 	 {Gothenburg, Sweden},
  publisher = {ACM},
  URL = {https://doi.org/10.1145/3183440.3194986},
  annote = 	 {7 references.}
}

@inproceedings{Singleton-Leavens14,
 author = {John L. Singleton and Gary T. Leavens},
 title = {Verily: A Web Framework for Creating More Reasonable Web Applications},
 booktitle = {Companion Proceedings of the 36th International Conference on Software Engineering},
 series = {ICSE Companion 2014},
 year = 2014,
 isbn = {978-1-4503-2768-8},
 location = {Hyderabad, India},
 pages = {560--563},
 numpages = 4,
 url = {http://doi.acm.org/10.1145/2591062.2591069},
 doi = {10.1145/2591062.2591069},
 acmid = 2591069,
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Method Router Response, Model View Controller, Verily framework, web frameworks},
}

@InProceedings{Singleton-Leavens16,
  author = 	 {John L. Singleton and Gary T. Leavens},
  title = 	 {Spekl: A Layered System for Specification Authoring, Sharing, and Usage},
  booktitle = {1026 IEEE 17th International Conference on Information Reuse and Integration (IRI), Pittsburgh},
  year = 	 2016,
  pages = 	 {126-133},
  month = 	 jul,
  url = {http://dx.doi.org/10.1109/IRI.2016.24},
  doi = {10.1109/IRI.2016.24},
  annote = 	 {16 references.}
}

@InProceedings{Tan-etal12,
 author =       {Shin Hwei Tan and Darko Marinov and
                 Lin Tan and Gary T. Leavens},
 title =        {{@tComment}: Testing {Javadoc} Comments
                 to Detect Comment-Code Inconsistencies},
 booktitle =    PROC # "Fifth International Conference on Software Testing,
                Verification and Validation (ICST 2012)",
 pages =        {260--269},
 month =        apr,
 year =         2012,
 address =      {Montreal, Canada},
 url =          {http://doi.ieeecomputersociety.org/10.1109/ICST.2012.106}
}
                  
@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."
}

@Article{Tran-Jorgensen-Larsen-Leavens17,
author="Peter W. V. Tran-J{\o}rgensen and Peter Gorm Larsen and Gary T. Leavens",
title="Automated translation of {VDM} to {JML}-annotated {Java}",
journal="International Journal on Software Tools for Technology Transfer",
year="2017",
pages="211-235",
volume=20,
number=2,
month=apr,
Annote="39 references.",
doi="10.1007/s10009-017-0448-3",
url="http://dx.doi.org/10.1007/s10009-017-0448-3"
}
                  
@proceedings{VSTTE10,
  key = {VSTTE},
  address =      {Edinburgh, UK},
  editor =       {Gary T. Leavens and Peter O'Hearn and Sriram K. Rajamani},
  title = 	 {Verified Software: Theories, Tools, Experiments (VSTTE)},
  booktitle = 	 {Verified Software: Theories, Tools, Experiments (VSTTE)},
  year = 	 2010,
  month = 	 aug,
  publisher =    SV,
  URL =          {\url{http://dx.doi.org/10.1007/978-3-642-15057-9}}
}

@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"
}