A Functional Scenario for Bytecode Verification of Resource Bounds


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.

In CSL 200418th International Conference on Computer Science Logic
  • 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). URL

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