A Functional Scenario for Bytecode Verification of Resource Bounds

We consider a scenario where (functional) programs in pre-compiled form are exchanged among untrusted parties. Our contribution is a system of annotations for the code that can be verified at load time so as to ensure bounds on the time and space resources required for its execution, as well as to guarantee the usual integrity properties. Specifically, 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.

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal-Zilio, Line Jakubiec
• Keywords: Automated Reasoning, CSL 2004, First-order Functional Language, Termination Verification, Usual Integrity Properties