Résumé de rapport du LIF

Téléchargement / Download : pdf 204k , ps.gz 176k , bibtex

Abstract

We give a formal model for a first order functional language to be executed on a stack machine and for a bytecode verifier that performs two kinds of static verifications : a type analysis and a shape analysis, that are part of a system used to ensure resource bounds. Both are instances of a general data flow analyzer due to Kildall. The generic algorithm and both of its instances are certified with the Coq proof assistant.

Keywords

Mobile code, formal verification, Calculus of Constructions

Résumé

Nous présentons un modèle formel pour un langage fonctionnel du premier ordre exécuté sur une machine à pile et pour un vérificateur de bytecode qui effectue deux types de vérifications statiques : une analyse de types et une analyse de formes. Les deux sont utilisées dans un système visant à garantir une borne des ressources et sont des instances d'un algorithme générique du à Kildall. L'algorithme et ses deux instances, sont certifiés dans l'assistant de preuves Coq.

Mots clés

Code mobile, vérification formelle, Calcul des Constructions

Bibtex

@TECHREPORT{24-2005,
    AUTHOR	= {Solange Coupet-Grimal and William Delobel},
    TITLE	= {{A Uniform and Certified Approach for Two Static Analyses}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {24-2005},
    MONTH	= {April},
    YEAR	= {2005},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/24-2005.html},
}