Skip to Main content Skip to Navigation
New interface
Reports (Research report)

A constraint-based algorithm for analysing memory usage on Java cards

Gerardo Schneider 1 
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We address in this paper the problem of statically determining whether a JavaCard applet may produce a memory overflow because of the dynamic instantiation of classes inside cycles. We provide a constraint-based algorithm which determines potential loops and (mutually) recursive methods. The algorithm operates on the byte-code of an applet. It is written as a set of rules -one for each byte-code instruction- which allows a compositional reasoning and it comprises both inter- and intra-procedural analysis. We aimed at an algorithm suitable to be fed into the proof assistant Coq in order to extract a certified memory usage analyser. We prove termination of the algorithm as well as its soundness and completeness with respect to an abstraction of the operational semantics of the language.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 8:53:52 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:20 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:28:59 PM


  • HAL Id : inria-00070567, version 1


Gerardo Schneider. A constraint-based algorithm for analysing memory usage on Java cards. [Research Report] RR-5440, INRIA. 2004, pp.26. ⟨inria-00070567⟩



Record views


Files downloads