Rapport 17-2004
Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio and Line Jakubiec
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.
On définit une simple machine à pile pour un langage fonctionnel du premier ordre et on montre comment mener des vérifications de type, de taille et de terminaison au niveau du code octet de la machine. En particulier, on montre qu'une combinaison de la vérification de taille basée sur les quasi-interprétations et de la vérification de terminaison basée sur un ordre récursif sur les chemins lexicographique mène à une borne explicite sur l'espace nécessaire à l'exécution.
@TECHREPORT{17-2004, AUTHOR = {Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio and Line Jakubiec}, TITLE = {{A Functional Scenario for Bytecode Verification of Resource Bounds}}, INSTITUTION = {{LIF}}, ADDRESS = {Marseille, France}, TYPE = {Research report}, NUMBER = {17-2004}, MONTH = {January}, YEAR = {2004}, NOTE = {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/17-2004.html}, }