About us
Espace utilisateur
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Home   /   Thesis   /   Combining over and under-approximations for low-level code analysis

Combining over and under-approximations for low-level code analysis

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges


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


Département Ingénierie Logiciels et Systèmes (LIST)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down