Certification of Memory Usage

  • Martin Hofmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


We describe a type-based approach for inferring heap space usage of certain functional programs and a mechanism for generating certificates as to the thus inferred memory consumption in the form of proofs in a VDM-style program logic fore Java bytecode (Java bytecode being the target of compilation). This gives a current snapshot of our work in the EU-funded project ‘Mobile Resource Guarantees’ between LMU-Munich and LFCS Edinburgh.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Martin Hofmann
    • 1
  1. 1.Institut für InformatikLudwig-Maximilians-Universität MünchenMünchenGermany

Personalised recommendations