% References for the Jive Data and Store Model

%misc
@string{AND  = " and "}

%authors
@string{a:APH    = "Arnd Poetzsch-Heffter"}
@string{a:JMG    = "Jean-Marie Gaillourdet"}
@string{a:NR     = "Nicole Rauch"}
@string{a:APH+JMG+NR = a:APH #AND# a:JMG #AND# a:NR}

%series
@string{LNCS     = {Lecture Notes in Computer Science}}

%publishers
@String{S-V =    "Springer-Verlag"}


@misc{ Jive,
  KEY = {Jive},
  TITLE = {Jive Project Webpage},
  NOTE = {\url{http://softech.informatik.uni-kl.de/softech/content/eforschung/e3490/index_ger.html}}
  }

@InCollection{ Leavens.BakerEA99jml,
  author =       {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
  editor =       {Haim Kilov and Bernhard Rumpe and Ian Simmonds},
  title =        {{JML}: A Notation for Detailed Design},
  booktitle =    {Behavioral Specifications of Businesses and Systems},
  pages =        {175--188},
  publisher =    {Kluwer},
  year =         {1999},
  chapter =      {12},
}

@InProceedings{ Meyer.Poetzsch-Heffter00architecture,
  Author =       "Meyer, J{\"o}rg and Poetzsch-Heffter, Arnd",
  Title =        "An Architecture for interactive Program Provers",
  BookTitle =    "{TACAS00}, Tools and Algorithms for the Construction
                  and Analysis of Systems",
  Editor =       "Graf, S. and Schwartzbach, M.",
  Year =         2000,
  Pages =        "63--77",
  SERIES =       LNCS,
  publisher =    S-V,
  VOLUME =       1785,
}

@misc{ Poetzsch-Heffter97specification,
  AUTHOR =       a:APH,
  TITLE =        { Specification and Verification of Object-Oriented
                  Programs } ,
  YEAR =         { 1997 },
  howpublished = { Habilitationsschrift, Technische Universit\"at
                  M\"unchen }
}

@techreport{ Poetzsch-Heffter.Gaillourdet.EA05hoare,
  author =       a:APH+JMG+NR,
  title =        "A {H}oare {L}ogic for a {J}ava {S}ubset and its
                  {P}roof of {S}oundness and {C}ompleteness",
  institution =  {University of Kaisers\-lautern, Germany},
  type =         "Internal Report",
  year =         2005,
  note =         "To appear"
}

