A Functional Scenario for Bytecode Verification of Resource Bounds

Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec
In CSL 2004 — 18th International Conference on Computer Science Logic, sep 2004.

 PDF  DOI〈10.1007/b100120〉

Abstract

#

We define a simple stack machine for a first-order functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.

References

#

• An abridged version of this paper was first presented at the 2nd workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE 2004).  Link

• An extended version appears as Research Report 17-2004, LIF, Jan. 2004.  PDF

Citation

#

@InProceedings{DalzilioS:fsbvrb,
   author    = {Amadio, Roberto M. and Coupet-Grimal, Solange and {Dal Zilio}, Silvano and Jakubiec, Line},
   title     = {{A Functional Scenario for Bytecode Verification of Resource Bounds}},
   booktitle = {CSL 2004 -- 18th International Conference on Computer Science Logic},
   series    = {Lecture Notes in Computer Science},
   volume    = {3210},
   publisher = {Springer-Verlag},
   doi = {10.1007/b100120},
   pages     = {265--279},
   month     = sep, 
   year      = 2004
}