HDR : A Modern Eye on Separation Logic for Sequential Programs

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)