% $Id: cheon.bib,v 1.32 2008/05/21 06:30:50 cheon Exp $

@string{ACM = "ACM"}
@string{LNCS = "Lecture Notes in Computer Science"}
%@String(SPandE = "Software---Practice and Experience")
@string{NY = "New York, NY"}
@string{SIGPLAN = "ACM SIGPLAN Notices"}

@InProceedings{Agarwal-etal07,
  Key =		 {Agarwal, {\it et al.}},
  Author =	 {Poonam Agarwal and Carlos E. Rubio-Medrano and
                  Yoonsik Cheon and Patricia J. Teller},
  Title =	 {A Formal Specification in {JML} of the {Java}
                  Security Package},
  Booktitle =	 {Advances and Innovations in Systems, Computing Science, 
                  and Software Engineering},
  Editor =       {Khaled Elleithy},
  Pages =        {363--368},
  Publisher =    {Springer},
  Year =	 2007
}

@TechReport{Agarwal-etal06a,
  Key =		 {Agarwal, {\it et al.}},
  Author =	 {Poonam Agarwal and Carlos E. Rubio-Medrano and
                  Yoonsik Cheon and Patricia J. Teller},
  Title =	 {A Formal Specification in {JML} of the {Java}
                  Security Package},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Apr,
  Year =	 2006,
  Number =	 {06-13},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr06-13.pdf}
}

@InProceedings{Browne-etal06,
  Author =	 {James C. Browne and Calvin Lin and Kevin Kane and
                  Yoonsik Cheon and Patricia J. Teller},
  Title =	 {Unification of verification and validation methods 
                  for software systems: progress report and initial 
                  case study formulation},
  BookTitle =	 {The 20th International Parallel and Distributed 
                  Processing Symposium (IPDPS 2006), Proceedings,
                  25-29 April 2006, Rhodes Island, Greece},
  Publisher =    {IEEE},
  Pages =        {1--7},
  Month =        Apr,
  Year =	 2006,
  URL =          {http://dx.doi.org/10.1109/IPDPS.2006.1639582}
}

@Article{Burdy-etal05,
  key =          {Burdy, {\it et al.}},
  author = 	 {Lilian Burdy and Yoonsik Cheon and David Cok and 
                   Michael Ernst and Joe Kiniry and Gary T. Leavens and 
                   K. Rustan M. Leino and Erik Poll},
  title = 	 {An overview of {JML} tools and applications},
  journal = 	 {International Journal on Software Tools 
                  for Technology Transfer (STTT)},
  volume =       7,
  number =       3,
  month =        Jun,
  year = 	 {2005},
  publisher =    {Springer-Verlag},
  pages =        {212--232}
}

@InProceedings{Cheon07,
   Key =       {Cheon},
   Author =    {Yoonsik Cheon},
   Title =     {Automated Random Testing to Detect Specification-Code
                Inconsistencies},
   Booktitle = {Proceedings of the 2007 International Conference 
                on Software Engineering Theory and Practice, 
                July 9-12, 2007, Orlando, Florida, U.S.A},
   Pages =     {112--119},
   Month =     Jul,
   Year =      2007,
}

@TechReport{Cheon07a,
  Key =		 {Cheon},
  Author =	 {Yoonsik Cheon},
  Title =	 {Automated Random Testing to Detect Specification-Code
                  Inconsistencies},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Feb,
  Year =	 2007,
  Number =	 {07-07},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr07-07.pdf},
  Note =         {To appear in \textit{SETP 2007}}
}

@InProceedings{Cheon07b,
   Key =       {Cheon},
   Author =    {Yoonsik Cheon},
   Title =     {Abstraction in Assertion-based Test Oracles},
   Booktitle = {Proceedings of the Seventh International Conference 
                on Quality Software, Portland, Oregon, USA, 
                October 11-12, 2007},
   Pages =     {410--414},
   Month =     Oct,
   Year =      2007,
   Publisher = {IEEE Computer Society}
}

@InProceedings{Cheon93,
  key =		 {Cheon},
  author =	 {Yoonsik Cheon},
  title =	 {Inheritance in Larch Interface Specification Languages,
                  Its Semantic Foundation and Formal Semantics},
  booktitle =	 {Proceedings of International Refinement Workshop
                  and Formal Methods Pacific (IRW/FMP '98),
                  29 September - 2 October 1998, Canberra, Australia},
  editor =       {Jim Grundy and Martin Schwenke and Trevor Vickers},
  publisher =    {Springer-Verlag},
  pages =        {81--99},
  month =        Sep,
  year =	 1998
}

@InProceedings{Cheon-Cho-Kim99,
  key =		 {Cheon \& Cho \& Kim},
  author =	 {Yoonsik Cheon and Soosun Cho and Heungnam Kim},
  title =	 {A Formal Specification of {DSM-CC} Interfaces},
  booktitle =	 {The First International Conference on Advanced 
                  Communication Technology, Muju Resorts, Korea,
                  February 10-12, 1999},
  year =	 1999
}

@TechReport{Cheon-Hayashi-Leavens03,
  Key =		 "Cheon \& Hayashi \& Leavens",
  Author =	 "Yoonsik Cheon and Yoshiki Hayashi and Gary
                  T. Leavens",
  Title =	 "A Thought on Specification Reflection",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Dec,
  Year =	 2003,
  Number =	 "03-16",
  Note =	 "Available from \url{archives.cs.iastate.edu}. To
                  appear in (SCI 2004).",
  Annote =	 "21 references."
}

@InProceedings{Cheon-Hayashi-Leavens04,
  Key =		 {Cheon \& Hayashi \& Leavens},
  Author =	 {Yoonsik Cheon and Gary T. Leavens},
  Title =	 {A Thought on Specification Reflection},
  BookTitle =	 {The 8th World Multi-Conference on Systemics, 
                  Cybernetics and Informatics (SCI 2004), 
                  July 18-21, 2004, Orlando, Florida, USA,
                  Volume II, Computing Techniques},
  Pages =	 {485-490},
  year =	 2004,
  Editor =	 {N. Callaos and W. Lesso and B. Sanchez},
}

@TechReport{Cheon-Kim05,
  Key =		 "Cheon \& Kim",
  Author =	 "Yoonsik Cheon and Myoung Kim",
  Title =	 "A Fitness Function for Modular Evolutionary Testing
                  of Object-Oriented Programs",
  Institution =	 "Department of Computer Science, 
                  The University of Texas at El Paso",
  Month =	 Oct,
  Year =	 2005,
  Number =	 "05-35",
  URL =          "http://www.cs.utep.edu/~cheon/techreport/tr05-35.pdf"
}

@InProceedings{Cheon-Kim06,
  Key =		 {Cheon \& Kim},
  Author =	 {Yoonsik Cheon and Myoung Kim},
  Title =	 {A Fitness Function for Evolutionary Testing
                  of Object-Oriented Programs},
  BookTitle =	 {Genetic and Evolutionary Computation Conference,
                  Seattle, WA, USA, July 8-12, 2006},
  Pages =	 {1952-1954},
  Month =	 Jul,
  Year =	 2006,
  Publisher =	 {ACM Press},
  Annote =       {An extended abstract of TR 05-35}
}


@InProceedings{Cheon-Kim-Perumandla05,
  Key =		 {Cheon \& Kim \& Perumandla},
  Author =	 {Yoonsik Cheon and Myoung Kim and 
                  Ashaveena Perumandla},
  Title =	 {A Complete Automation of Unit Testing for {Java} Programs},
  BookTitle =	 {Proceedings of the 2005 International Conference on
                  Software Engineering Research and Practice (SERP '05),
                  Volume I, Las Vegas, Nevada, June 27-29, 2005},
  Editor =	 {Hamid R. Arabnia and Hassan Reza},
  Pages =	 {290--295},
  Year =	 2005,
  Publisher =	 {CSREA Press}
}

@TechReport{Cheon-Kim-Perumandla05a,
  Key =		 "Cheon \& Kim \& Perumandla",
  Author =	 "Yoonsik Cheon and Myoung Kim and 
                  Ashaveena Perumandla",
  Title =	 "A Complete Automation of Unit Testing for Java Programs",
  Institution =	 "Department of Computer Science, 
                  The University of Texas at El Paso",
  Month =	 Feb,
  Year =	 2005,
  Number =	 "05-05",
  Note =         "To appear in SERP 2005",
  URL =          "http://www.cs.utep.edu/~cheon/techreport/tr05-05.pdf"
}

@InProceedings{Cheon-Kim99,
  key =		 {Cheon \& Kim},
  author =	 {Yoonsik Cheon and Heungnam Kim},
  title =	 {Specifying Behavioral Interface of Smalltalk Blocks},
  booktitle =	 {Proceedings of Asia-Pacific Software Engineering
                  Conference (APSEC '99), Takamatsu, Japan, 
                  December 7-10, 1999},
  year =	 1999,
  pages =        {468--475},
  publisher =    {IEEE Computer Society}
}

@InProceedings{Cheon-Kim-Oh98,
  key =		 {Cheon \& Kim \& Oh},
  author =	 {Yoonsik Cheon and Kangho Kim and Youngbae Oh},
  title =	 {Automatic Generation of {C++} Programs from
                  {LOTOS} Data Type Specifications},
  booktitle =	 {Proceedings of the IASTED Conference on 
                  Software Engineering, Las Vesaga, Nevada, USA,
                  October 28-31, 1998},
  editor =       {Roger Lee},
  pages =        {103--106},
  year =	 1998
}

@InProceedings{Cheon-Kim-Shin00,
  key =		 {Cheon \& Kim \& Shin},
  author =	 {Yoonsik Cheon and Heungnam Kim and Kyusang Shin},
  title =	 {A Software {MPEG-1} Decoder for {Internet-TV} Set-top
                  Boxes},
  booktitle =	 {The Second International Conference on
                  Advanced Communication Technology, Muju Resorts, Korea,
                  February 16--18, 2000},
  year =	 2000,
  pages =        {320--325}
}

@TechReport{Cheon-Leavens01,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Simple and Practical Approach to Unit Testing: The
                  {JML} and {JUnit} Way",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Nov,
  Year =	 2001,
  Number =	 "01-12",
  Note =	 "Available from archives.cs.iastate.edu.",
  Annote =	 "51 references."
}

@InProceedings{Cheon-Leavens02,
  key =		 {Cheon \& Leavens},
  author =	 {Yoonsik Cheon and Gary T. Leavens},
  title =	 {A Simple and Practical Approach to Unit Testing: The
                  {JML} and {JUnit} Way},
  booktitle =	 {ECOOP 2002 --- Object-Oriented Programming, 16th
                  European Conference, M\'{a}alaga, Spain,
                  Proceedings},
  pages =	 {231-255},
  year =	 2002,
  editor =	 {Boris Magnusson},
  volume =	 2374,
  series =	 LNCS,
  address =	 {Berlin},
  month =	 Jun,
  publisher =	 {Springer-Verlag},
  annote =	 {The jmlunit tool. 38 references.}
}

@TechReport{Cheon-Leavens02a,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Simple and Practical Approach to Unit Testing: The
                  {JML} and {JUnit} Way",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Mar,
  Year =	 2002,
  Number =	 "01-12a",
  Note =	 "Appears in ECOOP 2002 proceedings, LNCS 2374,
                  pp. 231-255.",
  Annote =	 "51 references."
}

@InProceedings{Cheon-Leavens02b,
  key =		 {Cheon \& Leavens},
  author =	 {Yoonsik Cheon and Gary T. Leavens},
  title =	 {A Runtime Assertion Checker for the {Java Modeling
                  Language (JML)}},
  booktitle =	 {Proceedings of the International Conference on
                  Software Engineering Research and Practice (SERP
                  '02), Las Vegas, Nevada, USA, June 24-27, 2002},
  pages =	 {322--328},
  year =	 2002,
  editor =	 {Hamid R. Arabnia and Youngsong Mun},
  month =	 Jun,
  publisher =	 {CSREA Press},
  annote =	 {23 references.},
  url =          {ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf}
}

@TechReport{Cheon-Leavens02c,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Runtime Assertion Checker for the {Java Modeling
                  Language (JML)}",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Mar,
  Year =	 2002,
  Number =	 "02-05",
  Note =	 "In SERP 2002, pp. 322-328",
  Annote =	 "19 references.",
  URL =          "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf"
}

@TechReport{Cheon-Leavens04,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "The {JML} and {JUnit} Way of Unit Testing and its
                  Implementation",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Apr,
  Year =	 2004,
  Number =	 "04-02a",
  Annote =	 "51 references.",
  URL =          "ftp://ftp.cs.iastate.edu/pub/techreports/TR04-02/TR.pdf"
}

@InProceedings{Cheon-Leavens05,
  key =		 {Cheon \& Leavens},
  author =	 {Yoonsik Cheon and Gary T. Leavens},
  title =	 {A Contextual Interpretation of Undefinedness
                  for Runtime Assertion Checking},
  booktitle =	 {AADEBUG 2005, 
                  Proceedings of the Sixth International Symposium
                  on Automated and Analysis-Driven Debugging,
                  Monterey, California, September 19--21, 2005},
  pages =	 {149--157},
  year =	 2005,
  month =	 Sep,
  publisher =	 {ACM Press},
  annote =	 {30 references.}
}

@TechReport{Cheon-Leavens05a,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Contextual Interpretation of Undefinedness
                  for Runtime Assertion Checking",
  Institution =	 "Department of Computer Science, 
                  The University of Texas at El Paso",
  Month =	 Mar,
  Year =	 2005,
  Number =	 "05-10",
  Note =         "To appear in AADEBUG 2005",
  URL =          "http://www.cs.utep.edu/~cheon/techreport/tr05-10.pdf"
}

@TechReport{Cheon-Leavens93a,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Quick Overview of {Larch/C++}",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Jun,
  Year =	 1994,
  Number =	 "93-18a",
  Note =	 "Appears in the {\em Journal of Object-Oriented
                  Programming}, 7(6):39-49, October 1994.",
  Annote =	 "29 references."
}

@Article{Cheon-Leavens94,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "The {Larch/Smalltalk} Interface Specification
                  Language",
  Journal =	 "ACM Transactions on Software Engineering and
                  Methodology",
  Month =	 Jul,
  Year =	 1994,
  Volume =	 3,
  Number =	 3,
  Pages =	 "221-253",
  Annote =	 "44 references."
}

@TechReport{Cheon-Leavens94b,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "The {Larch/Smalltalk} Interface Specification
                  Language",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 May,
  Year =	 1994,
  Number =	 "93-24a",
  Note =	 "Appeared in {\it ACM TOSEM}, July 1994, pages
                  221-253. Available by anonymous ftp from
                  ftp.cs.iastate.edu, and by e-mail from
                  almanac@cs.iastate.edu.",
  Annote =	 "44 references."
}

@TechReport{Cheon-Leavens94c,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A gentle introduction to {Larch/Smalltalk}
                  specification browsers",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Jan,
  Year =	 1994,
  Number =	 "94-01",
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR94-01/TR.ps.Z",
  Note =	 "Available by anonymous ftp from ftp.cs.iastate.edu,
                  and by e-mail from almanac@cs.iastate.edu."
}

@Article{Cheon-Leavens94d,
  Key =		 "Cheon \& Leavens",
  Author =	 "Yoonsik Cheon and Gary T. Leavens",
  Title =	 "A Quick Overview of {Larch/C++}",
  Journal =	 "Journal of Object-Oriented Programming",
  Year =	 1994,
  Volume =	 7,
  Number =	 6,
  Month =	 Oct,
  Pages =	 "39-49",
  Annote =	 "29 references."
}

@InProceedings{Cheon-Park-Shin01,
  key =		 {Cheon \& Park \& Shin},
  author =	 {Yoonsik Cheon and Sunghee Park and Kyusang Shin},
  title =	 {Formally Specifying Protocols and {APIs} of
                  Enterprise {JavaBeans}},
  booktitle =	 {The Third International Conference on
                  Advanced Communication Technology, Muju Resorts, Korea,
                  February 8-10, 2001},
  year =	 2001
}

@Article{Cheon-Perumandla06,
  Key =          {Cheon \& Perumandla},
  Author =       {Yoonsik Cheon and Ashaveena Perumandla},
  Title =        {Specifying and Checking Method Call Sequences of {Java} 
                  Programs},
  Journal = 	 {Software Quality Journal},
  Year =	 2006,
  Note =         {To appear}
}

@TechReport{Cheon-Perumandla06a,
  Key =		 {Cheon \& Perumandla},
  Author =	 {Yoonsik Cheon and Ashaveena Perumandla},
  Title =	 {Specifying and Checking Method Call Sequences 
                  of Java Programs},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Apr,
  Year =	 2006,
  Number =	 {05-36},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  Annote =       {Extended version of SERP 2006 paper},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr05-36.pdf}
}

@InProceedings{Cheon-Perumandla05,
  Key =		 {Cheon \& Perumandla},
  Author =	 {Yoonsik Cheon and Ashaveena Perumandla},
  Title =	 {Specifying and Checking Method Call Sequences in {JML}},
  BookTitle =	 {Proceedings of the 2005 International Conference on
                  Software Engineering Research and Practice (SERP '05),
                  Volume II, Las Vegas, Nevada, June 27-29, 2005},
  Editor =	 {Hamid R. Arabnia and Hassan Reza},
  Pages =	 {511--516},
  Year =	 2005,
  Publisher =	 {CSREA Press},
  URL =          "http://www.cs.utep.edu/~cheon/techreport/tr05-05.pdf"
}

@TechReport{Cheon-Perumandla05a,
  Key =		 "Cheon \& Perumandla",
  Author =	 "Yoonsik Cheon and Ashaveena Perumandla",
  Title =	 "Specifying and Checking Method Call Sequences in {JML}",
  Institution =	 "Department of Computer Science, 
                  The University of Texas at El Paso",
  Month =	 Feb,
  Year =	 2005,
  Number =	 "05-04",
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  Note =         "To appear in SERP 2005",
  URL =          "http://www.cs.utep.edu/~cheon/techreport/tr05-05.pdf"
}

@Article{Cheon-Perumandla07,
  Key =          {Cheon \& Perumandla},
  Author =       {Yoonsik Cheon and Ashaveena Perumandla},
  Title =        {Specifying and Checking Method Call Sequences of {Java} 
                  Programs},
  Journal = 	 {Software Quality Journal},
  Volume =       15,
  Number =       1,
  Month =        Mar,
  Year =	 2007,
  Pages =        {7--25},
  Publisher =    {Springer}
}

@InProceedings{Cheon-Rubio07,
  Key =		 {Cheon \& Rubio-Medrano},
  Author =	 {Yoonsik Cheon and Carlos E. Rubio-Medrano},
  Title =	 {Random Test Data Generation for Java Classes Annotated
                  with {JML} Specifications},
  Booktitle =	 {Proceedings of the 2007 International Conference
                  on Software Engineering Research and Practice,
                  Volume II, June 25--28, 2007, Las Vegas, Nevada},
  Pages =        {385--392},
  Month =	 Jun,
  Year =	 2007,
  Publisher =    {CSREA Press},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr07-11.pdf}
}

@TechReport{Cheon-Rubio07a,
  Key =		 {Cheon \& Rubio-Medrano},
  Author =	 {Yoonsik Cheon and Carlos E. Rubio-Medrano},
  Title =	 {Random Test Data Generation for Java Classes Annotated
                  with JML Specifications},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Mar,
  Year =	 2007,
  Number =	 {07-11},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  Note =         {To appear in SERP 2007},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr07-11.pdf}
}

@InProceedings{Cheon-Shin00,
  key =		 {Cheon \& Shin},
  author =	 {Yoonsik Cheon and Kyusang Shin},
  title =	 {Specifying Frame Properties in the Presence of Subclassing},
  booktitle =	 {Proceedings of the Fifteenth International Symposium
                  on Computer and Information Science (ISCIS XV), 
                  October 11-13, 2000, Istanbul, Turkey},
  editor =      {M.Y. Karsligil and A.G. Yavuz and M.E. Karsligil},
  pages =        {400--409},
  month =        Oct,
  year =	 2000
}

@InProceedings{Cheon-Wong94,
  key =		 {Cheon \& Wong},
  author =	 {Yoonsik Cheon and Johnny Wong},
  title =	 {A Tree-Based Algorithm to Find the k-th Value 
                  in Distributed Systems},
  booktitle =	 {Proceedings of the ISMM -International Conference 
                  on Intelligent Information Management Systems, 
                  Washington, DC, June 1-3, 1994},
  year =	 1994
}


@InProceedings{Cheon-etal99,
  key =		 {Cheon \& Kim \& Kim \& Oh},
  author =	 {Yoonsik Cheon and Kangho Kim and Cheolhong Kim and
                  Youngbae Oh},
  title =	 {From {LOTOS} to {C++}, Issues and Tool Development},
  booktitle =	 {Proceedings of the Seventeenth IASTED Applied Informatics
                 (AI '99), Australia, February 15-18, 1999},
  editor =       {M.H. Hamz},
  year =	 1999,
  pages =        {368--371},
  publisher =    {ACTA Press}
}

@TechReport{Cheon-etal03,
  Key =		 "Cheon \& Leavens \& Sitaraman \& Edwards",
  Author =	 "Yoonsik Cheon and Gary T. Leavens and Murali
                  Sitaraman and Stephen Edwards",
  Title =	 "Model Variables: Cleanly Supporting Abstraction in
                  Design By Contract",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Sep,
  Year =	 2003,
  Number =	 "03-10a",
  Note =	 "To appear in \emph{Software -- Practice \& Experience}.
                  Available from \url{archives.cs.iastate.edu}.",
  Annote =	 "39 references."
}

@TechReport{Cheon-etal04,
  Key =		 "Cheon \& Leavens \& Sitaraman \& Edwards",
  Author =	 "Yoonsik Cheon and Gary T. Leavens and Murali
                  Sitaraman and Stephen Edwards",
  Title =	 "Model Variables: Cleanly Supporting Abstraction in
                  Design By Contract",
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Month =	 Aug,
  Year =	 2004,
  Number =	 "03-10b",
  Note =	 "To appear in \emph{Software -- Practice \& Experience}.
                  Available from \url{archives.cs.iastate.edu}.",
  Annote =	 "26 references."
}

@Article{Cheon-etal05,
  Key =		 "Cheon \& Leavens \& Sitaraman \& Edwards",
  Author =	 "Yoonsik Cheon and Gary T. Leavens and Murali
                  Sitaraman and Stephen Edwards",
  Title =	 "Model Variables: Cleanly Supporting Abstraction in
                  Design By Contract",
  Journal = 	 SPandE,
  Year =	 2005,
  Volume =	 35,
  Number =	 6,
  Month =	 May,
  Pages =	 "583--599",
  Annote =	 "DOE: 10.1002/see.649"
}

@InProceedings{Cho-etal99,
  key =		 {Cho \& Cheon \& Kim \& Oh \& Kim},
  author =	 {Soosun Cho and Yoonsik Cheon and Kangho Kim and
                  Youngbae Oh and Heungnam Kim},
  title =	 {A {LOTOS} Toolset for Validating Communication Systems},
  booktitle =	 {The First International Conference on Advanced 
                  Communication Technology, Muju Resorts, Korea,
                  February 10-12, 1999},
  pages =        {384--389},
  year =	 1999
}

@InProceedings{Jung-etal07,
  Key =		 {Jung \& Rubio-Medrano \& Wong \& Cheon},
  Author =	 {Hyotaeg Jung and Carlos E. Rubio-Medrano and Eric Wong
                  and Yoonsik Cheon},
  Title =	 {Architectural Assertions: Checking Architectural
                  Constraints at Run-Time},
  Booktitle =	 {The 6th International Workshop on System and 
                  Software Architectures},
  Pages =        {604--607},
  Month =	 Jun,
  Year =	 2007,
  Note =         {Published in Proceedings of SERP 2007,
                  Volume II, June 25--28, 2007, Las Vegas, Nevada,
                  CSREA Press},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr07-18.pdf}
}

@TechReport{Jung-etal07a,
  Key =		 {Jung \& Rubio-Medrano \& Wong \& Cheon},
  Author =	 {Hyotaeg Jung and Carlos E. Rubio-Medrano and Eric Wong
                  and Yoonsik Cheon},
  Title =	 {Architectural Assertions: Checking Architectural
                  Constraints at Run-Time},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Apr,
  Year =	 2007,
  Number =	 {07-18},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  Note =         {Submitted to IWSSA 2007},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr07-18.pdf}
}

@InProceedings{Kim-Cheon08,
  Author =	 {Myoung Yee Kim and Yoonsik Cheon},
  Title =	 {A Fitness Function to Find Feasible Sequences 
                  of Method Calls for Evolutionary Testing 
                  of Object-Oriented Programs},
  BookTitle =	 {International Conference on Software Testing, Verification,
                  and Validation, Norway, April 9-11, 2008},
  Month =        Apr,
  Year =	 2008,
}

@TechReport{Leavens-Cheon92a,
  Key =		 "Leavens \& Cheon",
  Author =	 "Gary T. Leavens and Yoonsik Cheon",
  Title =	 "Preliminary Design of {Larch/C++}",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Address =	 "226 Atanasoff Hall, Ames IA 50011",
  Year =	 1992,
  Number =	 "92-16",
  Month =	 May,
  Note =	 "Presented at the First International Workshop on
                  Larch, Dedham, Mass., July, 1992.",
  Annote =	 "26 references."
}

@InCollection{Leavens-Cheon92b,
  Key =		 "Leavens \& Cheon",
  Author =	 "Gary T. Leavens and Yoonsik Cheon",
  Title =	 "Preliminary Design of {Larch/C++}",
  BookTitle =	 "Proceedings of the First International Workshop on
                  Larch, July, 1992",
  Publisher =	 "Springer-Verlag",
  Editor =	 "U. Martin and J. Wing",
  Series =	 "Workshops in Computing",
  Pages =	 "159-184",
  Address =	 NY,
  Year =	 1993,
  Annote =	 "26 references."
}

@TechReport{Leavens-Cheon93b,
  Key =		 "Leavens \& Cheon",
  Author =	 "Gary T. Leavens and Yoonsik Cheon",
  Title =	 "Extending {CORBA IDL} to Specify Behavior with
                  {Larch}",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Year =	 1993,
  Number =	 "93-20",
  Month =	 Aug,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR93-20/TR.txt",
  Note =	 "Presented at the OOPSLA '93 Workshop:
                  ``Specification of Behavioral Semantics in OO
                  Information Modeling''. Available by anonymous ftp
                  from ftp.cs.iastate.edu or by e-mail from
                  almanac@cs.iastate.edu.",
  Annote =	 "Discusses Larch/CORBA. 6 references."
}

@TechReport{Leavens-Cheon94d,
  Key =		 "Leavens \& Cheon",
  Author =	 "Gary T. Leavens and Yoonsik Cheon",
  Title =	 "Overview and Specification of the Built-in Types in
                  {Little Smalltalk}",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Year =	 1994,
  Number =	 "91-22a",
  Address =	 "226 Atanasoff Hall, Ames IA 50011",
  Month =	 Feb,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR91-22/TR.ps.Z",
  Note =	 "Available by anonymous ftp from ftp.cs.iastate.edu,
                  and by e-mail from almanac@cs.iastate.edu."
}

@TechReport{Leavens-Cheon-Cok05,
  Key =		 "Leavens \& Cheon \& Cok",
  Author =	 "Gary T. Leavens and Yoonsik Cheon and David R. Cok",
  Title =	 "Demonstration of {JML} Tools",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Address =	 "226 Atanasoff Hall, Ames IA 50011",
  Year =	 2005,
  Number =	 "05-13",
  Month =	 Apr,
  Note =	 "Available by anonymous ftp from ftp.cs.iastate.edu.",
  URL = 	 {ftp://ftp.cs.iastate.edu/pub/techreports/TR05-13/TR.pdf},
  Annote =	 "14 references."
}

@Unpublished{Leavens-etal02,
  Key =		 {Leavens \& Poll \& Clifton \& Cheon \& Ruby},
  Author =	 {Gary T. Leavens and Erik Poll and Curtis Clifton and
                  Yoonsik Cheon and Clyde Ruby},
  Title =	 {JML Reference Manual},
  Month =	 Aug,
  Year =	 2002,
  Note =	 {Department of Computer Science, Iowa State
                  University. Available from
                  {\url{http://www.jmlspecs.org}}}
}

@Unpublished{Leavens-etal03,
  Key =		 {Leavens \& Poll \& Clifton \& Cheon \& Ruby},
  Author =	 {Gary T. Leavens and Erik Poll and Curtis Clifton and
                  Yoonsik Cheon and Clyde Ruby and David R. Cok and
                  Joseph Kiniry},
  Title =	 {JML Reference Manual},
  Month =	 Apr,
  Year =	 2003,
  Note =	 {Department of Computer Science, Iowa State
                  University. Available from
                  {\url{http://www.jmlspecs.org}}}
}

@InCollection{Leavens-etal03a,
  Key =		 {Leavens, {\em et al.}},
  Author =	 {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton
                  and Clyde Ruby and David R. Cok},
  Title =	 {How the Design of {JML} Accommodates Both Runtime
                  Assertion Checking and Formal Verification},
  BookTitle =	 {Formal Methods for Components and Objects: First
                  International Symposium, FMCO 2002, Lieden, The
                  Netherlands, November 2002, Revised Lectures},
  Year =	 2003,
  Editor =	 {Frank S. de Boer and Marcello M. Bonsangue and
                  Susanne Graf and Willem-Paul de Roever},
  Series =	 LNCS,
  Volume =	 2852,
  Publisher =	 "Springer-Verlag",
  Address =	 "Berlin",
  Pages =        "262-284",
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-04/TR.pdf",
  Annote =	 "81 references."
}

@TechReport{Leavens-etal03b,
  Key =		 {Leavens, {\em et al.}},
  Author =	 {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton
                  and Clyde Ruby and David R. Cok},
  Title =	 {How the Design of {JML} Accommodates Both Runtime
                  Assertion Checking and Formal Verification},
  Institution =	 "Department of Computer Science, Iowa State
                  University",
  Year =	 2003,
  Number =	 "03-04",
  Address =	 "Ames, Iowa, 50011",
  Month =	 Mar,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR03-04/TR.pdf",
  Note =	 "Published in FMCO 2002 proceedings, LNCS 2852,
                  2003.",
  Annote =	 "81 references."
}

@Unpublished{Leavens-etal04a,
  Key =		 {Leavens \& Poll \& Clifton \& Cheon \& Ruby},
  Author =	 {Gary T. Leavens and Erik Poll and Curtis Clifton and
                  Yoonsik Cheon and Clyde Ruby and David R. Cok and
                  Joseph Kiniry},
  Title =	 {JML Reference Manual},
  Month =	 Jul,
  Year =	 2004,
  Note =	 {Department of Computer Science, Iowa State
                  University. Available from
                  {\url{http://www.jmlspecs.org}}}
}

@Article{Leavens-etal05,
  Key =		 {Leavens, {\em et al.}},
  Author =	 {Gary T. Leavens and Yoonsik Cheon and Curtis Clifton
                  and Clyde Ruby and David R. Cok},
  Title =	 {How the Design of {JML} Accommodates Both Runtime
                  Assertion Checking and Formal Verification},
  Journal =	 {Science of Computer Programming},
  Year =	 2005,
  Month =        Mar,
  Volume =       55,
  Number =       {1-3},
  Publisher =	 {Elsevier},
  Pages =        {185-208}
}

@Unpublished{Leavens-etal05a,
  Key =		 {Leavens \& Poll \& Clifton \& Cheon \& Ruby},
  Author =	 {Gary T. Leavens and Erik Poll and Curtis Clifton and
                  Yoonsik Cheon and Clyde Ruby and David R. Cok and
                  Joseph Kiniry},
  Title =	 {JML Reference Manual},
  Month =	 Apr,
  Year =	 2005,
  Note =	 {Department of Computer Science, Iowa State
                  University. Available from
                  {\url{http://www.jmlspecs.org}}}
}

@InProceedings{Perez-Cheon-Gates06,
  Key =		 {Perez \& Cheon \& Gates},
  Author =	 {Angelica B. Perez and Yoonsik Cheon and Ann Q. Gates},
  Title =	 {Canica: An {IDE} for the Java Modeling Language},
  BookTitle =	 {The 10th IASTED International Conference on 
                  Software Engineering and Applications,
                  November 13-15, 2006, Dallas, TX, USA},
  Pages =	 {32--37},
  year =	 2006,
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr06-36.pdf},
  Annote =       {http://www.actapress.com/Abstract.aspx?paperId=28876}
}

@TechReport{Perez-Cheon-Gates06a,
  Key =		 {Perez \& Cheon \& Gates},
  Author =	 {Angelica B. Perez and Yoonsik Cheon and Ann Q. Gates},
  Title =	 {Canica: An {IDE} for the Java Modeling Language},
  Institution =	 {Department of Computer Science, 
                  The University of Texas at El Paso},
  Month =	 Aug,
  Year =	 2006,
  Number =	 {06-36},
  Address =	 {500 West University Ave., El Paso, TX, 79968},
  URL =          {http://www.cs.utep.edu/~cheon/techreport/tr06-36.pdf},
  Note =         {To appear in {\em International Conference on Software
                  Engineering and Applications, Dallas, TX, 
                  November 13-15}}
}