Le stage est proposée par
Il est supervisé par
Il est possible de poursuivre en thèse sur des thèmes similaires.
1) VERSION FRANÇAISE
CONTEXTE DU STAGE
SUJET DU STAGE
Compilation Programme C vers Formules Logiques
afin d'analyser les programmes C à l'aide d'outils de déduction automatique
Chaque instruction d'un programme impératif peut-être traduite en implication logique par la méthode de calculs des plus faibles préconditions.
Un programme devient alors une conjonction de formules logiques (des clauses de Horn) que l'on peut donner à un solveur SMT (Satisfaction Modulo Theory)
pour ensuite le questionner sur les propriétées satisfaites par le programme et ainsi vérifier certaines propriétés de correction du programme
(pas de division par 0, pas d'accès en dehors des bornes d'un tableau,...).
Les clauses de Horn sont un format intéressant à plusieurs titres :
- un format indépendant du langage de programmation puisque la sémantique du langage est explicitée lors de la traduction en clauses de Horn.
- un format d'entrée de très nombreux moteurs de logique,
- un format d'échanges entre outils de vérification, simple à parser, à générer.
L'objectif du stage est d'écrire un compilateur C vers Clause de Horn en s'appyuant sur l'architecture de compilateur CompCert C
(seul compilateur certifié sans bogue en Coq).
Dans un premier temps il s'agit de définir la transformation en Ocaml, l'optimiser pour éliminer les formules triviales,
Et si le temps le permet l'incorporer dans la version Coq de CompCert et la prouver en Coq.
MOTS CLEFS
Compilation, Plus Faible Préconditon, Preuve de Programme, Sovleur Satisfaction Modulo Theory, Assistant de Preuve Coq.
PRÉ-REQUIS
Le candidat/la candidate devra
- connaître le langage C et les principes de compilation,
- avoir envie d'apprendre un nouveau langage (Ocaml),
- être à l'aide avec les raisonnements logiques,
- être intéressé par la preuve automatique
RÉFÉRENCES BIBLIOGRAPHIQUES
- Jean-Baptiste Tristan - PhD 2009 - Formal Verification of Translation Validators
(disponible sur le web, voir page 21 pour une liste de travaux sur la validation de traduction par des compilateurs)
2) ENGLISH VERSION
CONTEXT
Avionics, automotive, aerospace use embedded programs for automatic piloting.
To analyze and certify the behavior of these programs we use tools (Static Analysis, SAT solver and SMT) which carry out a symbolic analysis of the programs.
Such analysis can guarantee that a program respects safety properties such as "The speed of the machine will never exceed xxx miles/h".
At VERIMAG laboratory we develop such tools (in Ocaml, C, C ++) and we prove their correction in COQ.
SUBJECT OF THE INTERNSHIP
Compilation of C Programs into Logical Formulae
in order to analyse C programs using automatic deduction tools
Each instruction of an imperative program can be translated into logical implication by computing the weakest precondition.
A program then becomes a conjunction of logical formulas (Horn clauses) which can be provided to an SMT solver (Satisfaction Modulo Theory).
Then, it is possible to question the solver to discover the properties satisfied by the program and thus to guarantee some correctness properties of the program
(no division by zero, no out-of-bound access in an array,...).
The Horn clauses are an interesting format for several reasons:
- it is independent of the programming language since the semantics of the language is captured during the translation into Horn clauses
- this format is recognized by many logic engines,
- it is a good format for exchanges between verification tools, simple to parse, to generate.
The objective of the internship is to write a compiler from C to Horn Clause based on the compiler architecture CompCert
(a certified compiler with a well-defined semantics written in Coq).
The first step consists in definign the transformation in Ocaml, then to optimize it in order to remove useless implications
(by constant propagation, partial evaluation and elimination of tautology).
Second, if there is enough time, the utlimate goal is to incorporate the compilcation into Horn clauses it into the Coq version of CompCert
and prove it in Coq. This second part is more challenging, and therefore more suitable for M2 internship.
KEYWORDS
Compilation, weakest preconditon, proof of program, SMT Sovler, Modulo Theory satisfaction, Coq prover
PREREQUISITES
The applicant should
- know the C language and the principles of compilation,
- want to learn a new language (Ocaml)
- be at ease with logical reasoning,
- be interested in automatic proof.
BIBLIOGRAPHY
- Jean-Baptiste Tristan - PhD 2009 - Formal Verification of Translation Validators
(available at url: https://tel.archives-ouvertes.fr/tel-00437582/document
see page 21 for many references on Validation of Compiler Translations)
3) ILLUSTRATION SUR UN EXEMPLE
UN PROGRAMME
Ligne 1: x = 2 * y + 1 ;
Ligne 2: r = x * y
SA TRADUCTION EN IMPLICATIONS LOGIQUES
Impl. I1 : P1(2*y+1) ==> P1(x)
Obligation 1;2 : P1(x) =?=> P2(x+y)
Impl. I2 : P2(x*y) ==> P2(r)
où P1, P2 sont des propriétés portant sur les variables x,y,r aux différentes lignes du programmes.
APPLICATION
Supposons qu'on souhaite montrer qu'à la fin du programme "r est pair"
on donne alors les implications précédentes à un solveur avec P2 =def= Pair?
on obtient:
VÉRIFICATON À L'AIDE D'UN PROUVEUR
Le solveur construit la preuve suivante
Prenons P1 =def= Impair?
Lemma: Pair(2) ==> Pair(2*y).
"puisque 2 est pair alors 2*y est pair"
Lemma: Pair(2*y) ==> Impair(2*y+1).
... "alors 2*y+1 est impair"
Implication 1: Impair?(2*y+1) ==> Impair?(x)
... "alors x est impair après la ligne 1 du programme
Le lemme suivant permet de démontrer l'obligation (1;2)
Lemma: Impair?(x) / Impair?(y) ==> Pair?(x+y)
"si (Hypohthèse) y est impair alors x+y est pair"
Implication 2: Pair?(x+y) ==> Pair?(r)
... "alors r est pair"
CONCLUSION: si y est Pair (Hypothèse) alors r est pair à la ligne 2