Specifying and verifying heap space allocation with JML and ESC/Java2

Research output: Contribution to conferencePaperpeer-review

1 Downloads (Pure)


We examine JML’s support for specifying the heap space allocation of Java programs. In this report we restrict ourselves to specifying and verifying only allocation but not de-allocation. We identify some problems with with JML’s support and suggest alternatives. Also, we describe an implementation of heap space allocation verification in ESC/Java2. This implementation has been tested on small examples.
Original languageEnglish
Publication statusPublished - 2006
EventFormal Techniques for Java-like Programs - Nantes, France
Duration: 4 Jul 20064 Jul 2006


ConferenceFormal Techniques for Java-like Programs
Abbreviated titleFTfJP


  • heap space allocation
  • Java2
  • Java Modelling Language
  • Java classes


Dive into the research topics of 'Specifying and verifying heap space allocation with JML and ESC/Java2'. Together they form a unique fingerprint.

Cite this