Certification de programmes impératifs en logique dynamique : le cas du lambda-calcul avec références
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
We present a formal System of software verification, MLDL, dedicated to an untyped S\lambdaS-calculus with higher-order references (MLimp) and call-by-value evaluation. MLDL follows a certification approach which consists in proving the correspondence between a program and its specification. MLDL is based on a second-order dynamic logic which combines purely logical deduction steps with symbolic evaluation. There are three types of modality in MLDL: the box of dynamic logic is adapted to MLimp where each program is an expression, updates represents local modifications of the memory and a specific binder (the v-binder) supports allocation of new memory cell. The thesis consists oftwo parts: a syntactic part devoted to the presentation ofMLDL and a semantic part devoted to the construction of a model of MLDL in order to prove the consistency of the formalism. The model ofMLDL is built on a denotational model of MLimp where congruent (through symbolic evaluation) programs belong to the same équivalence class. This denotational model is built with standard techniques ofsolving equations in the category ofdcpos and the category of cpos with injections- projections. We also develop a theory ofgroup action on the dcpo (especially applied to the group of permutations of addresses) and a notion of domination over programs and stores by a set of addresses. These new tools allow to deal with issues of well-foundness and invariance associated with the manipulation of memory locations.
Abstract FR:
Nous présentons un système formel de certification de fiabilité logicielle, MLDL, dédié à un lambda-calcul non typé contenant des références d'o/\ supérieur (MLimp). MLDL est basé sur une logique dynamique (DL) du second ordre dont le système déductif combine des étapes de déduction purement logiques et des étapes d'évaluation symbolique. Les modalités spécifiques de MLDL sont de trois types: les boîtes standard de DL sont adaptées à MLimp où tout programme est une expression, les updates permettent de représenter les modifications de la mémoire et un le v-lieur prend en charge l'allocation de nouvelles adresses. La thèse comporte deux volets : un volet syntaxique consacré à la présentation de MLDL, et un volet sémantique consacré à la construction d'un modèle de MLDL afin de prouver la cohérence du formalisme. Ce modèle est construit à partir d'un modèle dénotationnel de MLimp construit avec des techniques standard de résolution d'équations dans la catégorie des dcpo et la catégorie des cpo avec injections-projections. Nous développons également une théorie des actions de groupe sur les dcpo (appliquée en particulier au groupe des permutations d'adresses) ainsi que la relation de domination qui nous permettent de traiter les questions d'invariance liées à la manipulation des adresses mémoire.