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

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 programapos;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. [POPLapos;23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award) [VMCAIapos;22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival [RTASapos;21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award) [LPARapos;18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre

Your profile: Master's degree in computer science or engineering school. Background in static verification/analysis, programming in OCaml, knowledge of C or assembler, would be an advantage.