HDR defense: Arthur CHARGUERAUD
Abstract :
Separation Logic brought a major breakthrough in the area of program verification. Since its introduction, Separation Logic has made its way into a number of practical tools that are used on a daily basis for verifying programs, ranging from operating systems kernels and file systems to data structures and graph algorithms. These programs are written in a wide variety of programming languages at different abstraction levels, ranging from machine code and assembly, to C, Java, OCaml, and Rust, just to name a few. Numerous extensions to Separation Logic have been proposed over the past two decades. My habilitation manuscript presents an overview of my own contributions---and that of my co-authors---over the period from 2009 to 2022.
The manuscript is organized in three main parts. The first part describes a foundational set up of Separation Logic, with the logic being proved sound with respect to a semantics mechanized in an interactive proof assistant. The presentation targets an imperative lambda-calculus, sufficiently minimalistic to allow for an easy-to-teach presentation of the theory, yet sufficiently rich to support the verification of realistic programs. The second part presents the technique of characteristic formulae, which enables smooth proofs of practical programs in a proof assistant. Compared with the characteristic formulae introduced in my PhD thesis, I here give a simplified presentation based on weakest preconditions and, most importantly, I show how to justify characteristic formulae in a foundational manner. The third part of this manuscript describes extensions to Separation Logic for resource analysis: time credits for establishing amortized execution bounds, big-O notation to support asymptotic reasoning, and space credits to establish space bounds in the presence of a garbage collector.
The jury is made up of :
- Sandrine Blazy, Examiner, Professor, Université Rennes 1
- Dominique Devriese, Reviewer, Professor, KU Leuven
- Derek Dreyer, Professor, Max Planck Institute (MPI-SWS)
- Bob Harper, Reviewer, Professor, Carnegie Mellon University (CMU)
- Philippe Helluy, Examiner, Professeur, Université de Strasbourg
- Nicolas Magaud, Examiner, MdC HDR, Université de Strasbourg
- Xavier Rival, Reviewer, Directeur de recherche, Inria
Date : Monday 27th February 2023, 14h30
Place : salle de conférence de l'IRMA (7 Rue René Descartes, Strasbourg)
Le dépôt des candidatures pour les postes d’enseignants-chercheur est ouvert. Les offres sont...
Le salon Pollutec est l'événement international de référence des solutions pour l'environnement...
Le salon Pollutec est l'événement international de référence des solutions pour l'environnement...
Haitao Ge, doctorant à l'INSA Strasbourg au sein de l'équipe Génie civil - énergétique (GCE) a...
Dans le cadre du projet Interreg Offensive Science 2PhaseEx, cinq membres de l’équipe ICube/Mécaflu...
Le 13 novembre, le CNRS a réuni les 26 start-up issues de ses laboratoires sous tutelle,...
L'équipe de l'Université de Strasbourg et la délégation Alsace du CNRS se sont brillamment...
Le vendredi 20 septembre a eu lieu la réunion de lancement du projet INTERREG 2PhaseEx, au...
Le projet ENERGETIC a lancé sa première vidéo promotionnelle illustrant les principaux objectifs et...
Paris 27 aout 2024 – ARCHOS annonce que POLADERME, filiale du Startup studio Medtech du groupe...
Les topographes de l’INSA Strasbourg exerçant leurs activités de recherche au sein de l’équipe...