Nous interagissons de plus en plus avec des objets pilotés par des programmes. Dans cette thèse, nous allons nous intéresser à la définition d'analyses statiques correctes pour langages de programmation. Une analyse statique analyse du code sans l'exécuter. Elle peut garantir certaines propriétés d'un programme, par exemple, montrer qu'il n'y a pas de division par zéro. Nous souhaitons définir des analyses correctes, c'est-à-dire avec une preuve formelle, mathématique, que les analyses calculent effectivement les propriétés attendues. Pour atteindre ces objectifs, notre approche est de partir d'une description formelle d'un langage de programmation, et d'en dériver une interprétation abstraite. L'interprétation abstraite est une méthode de calcul d'approximations des comportements des programmes, et d'en déduire des propriétés sur ces programmes. Nous avons choisi les Sémantiques Squelettiques comme cadre pour formaliser des langages de programmation, car elles sont simples, mais très expressives. Une sémantique squelettique est une description partielle d'un langage. En complétant cette description, on peut obtenir une sémantique du langage, autrement dit une description mathématique de l'exécution des programmes de ce langage. Notre objectif est d'obtenir une sémantique et une interprétation abstraite à partir de la sémantique squelettique d'un langage, et de montrer que l'interprétation abstraite est une bonne approximation de la sémantique du langage.
(Un pot aura lieu en salle Lipari).
[ATTENTION dans le cadre du plan VIGIPIRATE : l’accès du public à cette soutenance est contraint à une inscription préalable obligatoire auprès de lydie [*] mabil
inria [*] fr. L’accès ne sera pas autorisé sans inscription préalable. Par ailleurs, les visiteurs ne porteront ni bagage ni sac.]
---------
PhD defense by Vincent Rébiscoul on May 14th, 2024, at 10:00 am in the Petri-Turing room at the Inria Center of the University of Rennes.
Abstract :
We interact more and more with objects that run code. In this Thesis, we will study the definition of static analyses of code for programming languages. A static analysis analyses code without executing it. It can show that a program guarantees some properties: for example, that no division by zero can occur in a given program. We wish to define correct static analysis, meaning that we want a formal mathematics proof that the analyses indeed compute the properties they are meant to compute. To meet these goals, our approach starts from the formal description of a language and to derive an abstract interpretation from it. The abstract interpretation is a method of approximation of the semantics of programs to deduce properties of these programs. We have chosen Skeletal Semantics as the framework to formalise programming languages, because of their simplicity but strong expressivity. A skeletal semantics is a partial description of a language. By completing this description, one can get a semantics for the language: a mathematical description of the behaviour of programs of this language. Our objective is to get a semantics and an abstract interpretation from a skeletal semantics, and to show that the abstract interpretation is a correct approximation of the semantics of the language.
(A reception will take place in the room Lipari).
-----------------
Public access to this event is subject to registration with lydie [*] mabilinria [*] fr - Access will not be permitted without prior registration. Visitors are not allowed to bring luggage or bags.
- Tom HIRSCHOWITZ, Rapporteur, Directeur de Recherche, LAMA
- Antoine MINÉ, rapporteur, Professeur, Sorbonne Université
- Anne-Cécile ORGERIE, Examinatrice, Directrice de Recherche, CNRS/IRISA
- Thomas JENSEN, Directeur de thèse, Directeur de Recherche, INRIA Rennes
- Alan SCHMITT, Co-directeur de thèse, Directeur de Recherche, INRIA Rennes