DELMAS David

Doktor
Forschungsgruppe : APR
Datum, an dem das LIP6 verlassen wurde : 30.06.2023
https://lip6.fr/David.Delmas

Forschungsleitung (Direction de recherche) : Antoine MINÉ

Co-Betreuung : SOUMIER Vincent (Airbus)

Static analysis of program portability by abstract interpretation

Computer programs tend to be used much longer than expected at design time, and in a wider variety of environments. Adapting a software product for new usage may turn out to be difficult and costly. Ensuring the portability of programs is a major stake: it amounts to ensuring that their compilation and execution in a different environment will have small controlled impact on their semantics.
The goal of this thesis is to develop a novel class of static analyses by abstract interpretation, allowing to verify portability properties of low-level C programs, i.e. programs whose behaviors depend on the representation of computer memory.
Portability verification aims at proving the equivalence of two syntactically close versions of a program running in different environments. We first focus on the particular case of regression verification, which aims at proving the equivalence of two program versions running in the same environment. We propose a static analysis of software patches that is able to infer such equivalence properties, in particular in the context of low-level C programs such as those used in embedded software.
Then we develop an approach to portability analysis of C programs that is designed as an extension of patch analysis. We focus on two portability properties, related to the representation of the computer memory specified by the ABI: portability against different representations of scalars (endianness), and against different memory layouts (offsets of scalar fields in C structs).
We implemented a prototype static analyzer on top of the MOPSA platform, and experimented it on real-world open source and industrial software. It allows successful analyses of large, real-world avionics software up to one million lines of C.

Verteidigung einer Doktorarbeit : 28.11.2022

Mitglieder der Prüfungskommission :

YAHAV Eran (Technion, Israel) [Rapporteur]
CHANG Bor-Yuh Evan (University Colorado Boulder, USA) [Rapporteur]
MINÉ Antoine (Sorbonne Université/LIP6)
CHAILLOUX Emmanuel (Sorbonne Université/LIP6)
FERET Jérôme (INRIA/ENS-DI)
PUTOT Sylvie (École Polytechnique)
SOUMIER Vincent (Airbus)
OUADJAOUT Abdelraouf

Datum, an dem das LIP6 verlassen wurde : 30.06.2023

Publikationen 2015-2022

Mentions légales
Plan