PhD graduated
Team : APR
Departure date : 06/30/2023

Supervision : Antoine MINÉ

Co-supervision : 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.

Defence : 11/28/2022

Jury members :

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

Departure date : 06/30/2023

2015-2022 Publications

Mentions légales
Site map