refs.bib

@STRING{lnai = "LNCS"}
@STRING{lncs = "LNCS"}
@STRING{spv = "Springer-Verlag"}

@book{KeYBook2016,
	booktitle = {Deductive Software Verification - The KeY Book - From Theory to Practice},
	title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
	editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Peter H. Schmitt and Mattias Ulbrich},
	doi = {10.1007/978-3-319-49812-6},
	isbn = {978-3-319-49811-9},
	year  = {2016},
	month = dec,
	volume = {10001},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	keywords = {},
	tppubtype = {book}
}

@inbook{Steinhoefel2019,
	author = {Dominic Steinh{\"o}fel and Reiner H{\"a}hnle},
	address = {Berlin},
	language = {en},
	month = {October},
	title = {Abstract Execution},
	pages = {319--336},
	booktitle = {Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings},
	year = {2019},
	publisher = {Springer},
	url = {http://tubiblio.ulb.tu-darmstadt.de/117206/},
	doi = {10.1007/978-3-030-30942-8\_20}
}



@Book{KeYBook2007,
   editor =        {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title =         {Verification of Object-Oriented Software: The {KeY} Approach},
   series        = {LNCS 4334},
   publisher     = spv,
   year          = {2007}
}

@InProceedings{BeckertGladisch2007,
  author =       {Bernhard Beckert and Christoph Gladisch},
  title =        {White-box Testing by Combining Deduction-based Specification Extraction and
                  Black-box Testing},
  booktitle =    {Proceedings, International Conference on Tests and Proofs (TAP),
                  Zurich, Switzerland},
  editor =       {B. Meyer and Y. Gurevich},
  publisher =    {Springer},
  series =       {LNCS 4454},
  year =         {2007}
}

@PhdThesis{SchlagerPhD2007,
  author =       {Steffen Schlager},
  title =        {Symbolic Execution as a Framework for Deductive Verification of Object-Oriented Programs},
  school =       {Fakult\"at f\"ur Informatik der Universit\"at Karlsruhe},
  month =        {February},
  year =         {2007},
  publisher =    {Sierke-Verlag}
}

@PhdThesis{RothPhD2006,
  author =       {Andreas Roth},
  title =        {Specification and Verification of Object-oriented Components},
  school =       {Fakult\"at f\"ur Informatik der Universit\"at Karlsruhe},
  month =        {June},
  year =         {2006}
}

@article{KeY2005,
  author        = {Wolfgang Ahrendt and Thomas Baar and
                   Bernhard Beckert and Richard Bubel and
                   Martin Giese and Reiner H\"ahnle and
                   Wolfram Menzel and Wojciech Mostowski and
                   Andreas Roth and Steffen Schlager and
                   Peter H. Schmitt},
  title         = {The {KeY} Tool},
  journal       = {Software and System Modeling},
  volume        = {4},
  pages         = {32-54},
  year          = {2005},
  doi           = {http://springerlink.metapress.com/openurl.asp?genre=article&id=doi:10.1007/s10270-004-0058-x},
  publisher     = spv
}


@InProceedings{Beckert01,
  author =       {Bernhard Beckert},
  title =        {A Dynamic Logic for the Formal Verification of
		  {J}ava {C}ard Programs},
  booktitle =    {Java on Smart Cards: Programming and
		  Security. Revised Papers, Java Card 2000,
		  International Workshop, Cannes, France},
  editor =       {I. Attali and T. Jensen},
  pages =        {6--24},
  publisher =    spv,
  series =       {LNCS 2041},
  year =         {2001}
}

@MastersThesis{Schlager02,
  author        ={Steffen Schlager},
  title         ={{H}andling of {I}nteger {A}rithmetic in the
                 {V}erification of {J}ava {P}rograms},
  school        ={{U}niversit\"at {K}arlsruhe},
  note          ={Available at:
		  \url{http://i12www.ira.uka.de/~key/doc/2002/DA-Schlager.ps.gz}},
  year          ={2002},
}


@techreport{KeY2003,
   author        = {Wolfgang Ahrendt and Thomas Baar and
                    Bernhard Beckert and Richard Bubel and
                    Martin Giese and Reiner H\"ahnle and
                    Wolfram Menzel and Wojciech Mostowski and
                    Andreas Roth and Steffen Schlager and
                    Peter H. Schmitt},
   title         = {The {K}eY {T}ool},
   institution   = {Department of Computing Science, Chalmers University
                    and G\"oteborg University, G\"oteborg, Sweden},
   type          = {Technical Report in Computing Science No.\ 2003-5},
   month         = feb,
   year          = {2003},
   note          = {Available at: \url{http://i12www.ira.uka.de/~beckert/pub/key03.pdf}}
}

@Misc{ESC,
  key =          {ESC},
  title =        {{ESC/Java} ({E}xtended {S}tatic {C}hecking for {J}ava)},
  note =         {\url{http://research.compaq.com/SRC/esc/}}
}

@InProceedings{Haehnle00a,
  author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
                  and Martin Giese and Elmar Habermalz and Reiner
                  H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
  title =        "The {KeY} Approach: {I}ntegrating Object Oriented
                  Design and Formal Verification",
  editor =       "Manuel Ojeda-Aciego and Inma P. de Guzm\'{a}n and
                  Gerhard Brewka and Lu\'{\i{}}s Moniz Pereira",
  series =       lnai,
  pages =        "21--36",
  volume =       1919,
  month =        oct,
  year =         "2000",
  booktitle =    "Proc.\ 8th European Workshop on Logics in AI (JELIA), Malaga, Spain",
  publisher =    spv,
}


@book{Meyer97,
 author     = "Meyer, Bertrand",
 title      = "Object-Oriented Software Construction (Second Edition)",
 publisher  = "Pren{\-}tice-Hall",
 isbn_issn = "0-13-629155-4",
 year       = 1997,
}

@Unpublished{JMLReferenceManual11,
  Author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik
            Cheon and Clyde Ruby and David Cok and Peter Müller and Joseph
             Kiniry and Patrice Chalin and Daniel M. Zimmerman},
  Title =	 {JML Reference Manual},
  Month =	 jul,
  Year =	 2011,
  Note =	 {Department of Computer Science, Iowa State
                  University. Available from
                  {\url{http://www.jmlspecs.org}}}
}

@TechReport{Leavens-Baker-Ruby04,
  Key =		 "Leavens \& Baker \& Ruby",
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "Preliminary Design of {JML}: A Behavioral Interface
                  Specification Language for {Java}",
  Institution =	 "Iowa State University, Department of Computer
                  Science",
  Year =	 2004,
  Number =	 "98-06y",
  Month =	 Nov,
  URL =
                  "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz",
  Annote =	 "79 references.",
  Note =	 "See \url{http://www.jmlspecs.org}."
}

@Unpublished{umlkeyquicktour,
  author = 	 {Thomas Baar and Reiner H{\"a}hnle and Steffen Schlager},
  title = 	 {KeY Quicktour},
  note = 	 {See \url{http://www.key-project.org/download/}}
}


@Misc{ICS,
  key = {ICS},
  note = {\url{http://www.icansolve.com}}
}

@Misc{Simplify,
   key  = {Simplify},
   note = {\url{http://secure.ucd.ie/products/opensource/ESCJava2/}}
}

@Misc{JavaReduxAPI,
   key = {Redux},
   title = {{J}ava{R}edux - {API}},
   note = {API documentation of a restricted subset of the Java Standard Library Classes.},
   url = {https://git.key-project.org/key-public/key/-/tree/stable/key/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux}
}

@MISC{RanTin-SMTLIB,
  author =	 {Clark Barrett and Silvio Ranise and Aaron Stump and Cesare Tinelli},
  title =	 {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
  howpublished = {{\tt www.SMT-LIB.org}},
  year =	 2008,
}


@InProceedings{EngelHaehnle07,
  author = 	 {Christian Engel and Reiner H\"{a}hnle},
  title = 	 {Generating Unit Tests from Formal Proofs},
  booktitle =	 {Proc.\ Tests and Proofs (TAP), Z\"{u}rich, Switzerland},
  year =	 {2007},
  editor =	 {Bertrand Meyer and Yuri Gurevich},
  series =	 lncs,
  volume = {4454},
  publisher =	 spv
}

@MISC{Engel05,
        AUTHOR             = {Christian Engel},
        HOWPUBLISHED       = {Studienarbeit, {F}akult\"{a}t f\"{u}r Informatik, {U}niversit\"{a}t {K}arlsruhe},
        MONTH              = jan,
        TITLE              = {A translation from JML to Java Dynamic Logic},
        YEAR               = {2005}
}
@phdthesis{Weiss2011,
  author       = {Benjamin Wei{\ss}},
  title        = {Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction},
  school       = {Karlsruhe Institute of Technology},
  year         = {2011}
}