@article{Jonkers1981,
author = {Hans M B Jonkers},
title = {Abstract storage structures},
journal = {Algorithmic languages},
publisher = {Noth-Holland},
year = 1981
}

@inproceedings{Deutsch1992,
author = {Alain Deutsch},
title = {A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations},
booktitle = {Proceedings of the International Conference on Computer Languages},
pages = {2--13},
publisher = {IEEE},
month = apr,
year = 1992
}

@article{Reddy1996,
author = {Uday S. Reddy},
title = {Global state considered unnecessary: An introduction to object-based semantics}, 
journal = {Journal of Lisp and Symbolic Computation},
volume = 9,
year = 1996,
pages = {7-76}
}

@inproceedings{HaehnleM:Cassis2005,
title = {Verification of Safety Properties in the Presence of Transactions},
author = {Reiner H\"ahnle and Wojciech Mostowski},
booktitle = {Post Conference Proceedings of CASSIS: Construction and Analysis of Safe, Secure and Interoperable Smart devices}, 
publisher = {Springer}, 
series = {LNCS}, 
volume = 3362,
pages = {151-171}, 
year = 2005
}

@article{BannwartMueller05,
 author = {Fabian Y. Bannwart and Peter M{\"u}ller},
 title = {A Logic for Bytecode},
 pages = {255--273},
 booktitle = {Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE)},
 editor = {Fausto Spoto},
 year = 2005,
 journal = {Electronic Notes in Theoretical Computer Science},
 volume = {141},
 number = {1},
 publisher = {Elsevier}
}

@unpublished{BeringerHofmannMobiusLogicProposal1.6,
  author = {Lennart Beringer and Martin Hofmann},
  title = {A new proposal for a logic for Mobius, Version 1.6},
  month = {January 20th},
  year = 2006,
  note = {Communicated by email to Mobius Bytecode-logicians}
}


@inproceedings{HofmannJost:POPL2003,
  author = {Martin Hofmann and Steffen Jost},
  title = {Static prediction of heap space usage for first-order functional programs},
  booktitle = {Proceedings of the 30th {ACM} Symposium on Principles of Programming Languages (POPL'03)}, 
  location = {New Orleans}, 
  month = jan,
  year = 2003,
  isbn = {1-58113-628-5},
  pages = {185--197},
  doi = {http://doi.acm.org/10.1145/604131.604148},
  publisher = {ACM Press}
}

@INPROCEEDINGS{BeringerHofmannMomiglianoShkaravska:LPAR2004,
  AUTHOR = {Lennart Beringer and Martin Hofmann and Alberto
                  Momigliano and Olha Shkaravska},
  TITLE = {Automatic Certification of Heap Consumption},
  BOOKTITLE = {LPAR 2004},
  PAGES = {347--362},
  YEAR = {2005},
  EDITOR = {Franz Baader, Andrei Voronkov},
  VOLUME = {3425},
  OPTNUMBER = {},
  SERIES = {LNCS},
  OPTMONTH = {Feb},
  PUBLISHER = {Springer-Verlag},
  OPTNOTE = {ISBN: 3-540-25236-3},
  PDF = {lpar.pdf}
}

@INPROCEEDINGS{CaJePiSc05MemoryUsage,
  AUTHOR = {David Cachera and Thomas Jensen and David Pichardie and Gerardo Schneider},
  TITLE = {Certified Memory Usage Analysis},
  PAGES = {91--106},
  BOOKTITLE = {Proceedings of the 13th International Symposium on Formal Methods (FM'05)},
  YEAR = {2005},
  PUBLISHER = {Springer-Verlag},
  VOLUME = {3582},
  SERIES = {LNCS}
}

@unpublished{VDMLogicForBytecode,
  title = {A {VDM}-style logic for bytecode},
  author = {Lennart Beringer and Martin Hofmann},
  note = {Available from the Mobius Wiki},
  month = oct,
  year = 2005
}

@inproceedings{DBLP:conf/aplas/BeringerH06,
  author    = {Lennart Beringer and
               Martin Hofmann},
  title     = {A Bytecode Logic for {JML} and Types},
  pages     = {389-405},
  ee        = {https://doi.org/10.1007/11924661_24},
  crossref  = {DBLP:conf/aplas/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aplas/2006,
  editor    = {Naoki Kobayashi},
  title     = {Proceedings of the 4th Asian Symposium on Programming Languages
               and Systems (APLAS 2006)}, 
  booktitle = {Proceedings of the 4th Asian Symposium on Programming Languages
               and Systems (APLAS 2006)}, 
  location  = {Sydney, Australia, November 8-10, 2006},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4279},
  year      = {2006},
  isbn      = {3-540-48937-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Misc{MobiusDeliverable3.1,
  author =       {{\sc Mobius }Consortium},
  title =        {Deliverable~3.1: Bytecode Specification Language and Program
                  Logic},
  year =         2006,
  keywords =     {mobius, wp3},
  note =         {Available online from \url{http://mobius.inria.fr}}
}

@Unpublished{Pichardie06,
  author =       "D. Pichardie",
  title =        "{Bicolano -- Byte Code Language in Coq}",
  note =         "{\url{http://mobius.inria.fr/twiki/bin/view/Bicolano}. Summary appears in
                  \cite{MobiusDeliverable3.1}}",
  year =         "2006"
}
  