General information
Organisation
The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas :
• defence and security,
• nuclear energy (fission and fusion),
• technological research for industry,
• fundamental research in the physical sciences and life sciences.
Drawing on its widely acknowledged expertise, and thanks to its 16000 technicians, engineers, researchers and staff, the CEA actively participates in collaborative projects with a large number of academic and industrial partners.
The CEA is established in ten centers spread throughout France
Reference
SL-DRT-24-0543
Direction
DRT
Thesis topic details
Category
Technological challenges
Thesis topics
Combining over and under-approximations for low-level code analysis
Contract
Thèse
Job description
Because program analysis is an undecidable problem, static analyzes fall into 2 categories:
- Sound analyses, which calculate an over-approximation of all the program's behaviors, and make it possible to verify the absence of errors.
- Complete analyses, which calculate an under-approximation of the possible behaviors of the program, and allow errors to be found.
The aim of the thesis is to study this combination of techniques for the verification of low-level programs, in particular binary executables, by targeting in particular the analyzes of memories and control flow, which are the capital information for understanding the possible behaviors of a binary executable.
[POPL'23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award)
[VMCAI'22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[RTAS'21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award)
[LPAR'18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre
University / doctoral school
Sciences et Technologies de l’Information et de la Communication (STIC)
Paris-Saclay
Thesis topic location
Site
Saclay
Requester
Position start date
01/10/2024
Person to be contacted by the applicant
LEMERRE Matthieu 
matthieu.lemerre@cea.fr
CEA
DRT/DILS//LSL
CEA - Centre de Saclay BP 94
F91191 Gif sur Yvette CEDEX
01 69 08 26 28
Tutor / Responsible thesis director
LEMERRE Matthieu matthieu.lemerre@cea.fr
CEA
DRT/DILS//LSL
CEA - Centre de Saclay BP 94
F91191 Gif sur Yvette CEDEX
01 69 08 26 28
En savoir plus
