Dr. Marc Chevalier

I'm developing the engine behind our fast multi-language code analyzer. To make it scalable with respect to the number of supported languages, the input code is compiled to a common intermediate representation, which is analyzed thanks to ML-powered security rules.

Teacher of math in 1st year of FDV bachelor in CRI, Paris. 104h The curriculum involves logic, set theory, basic function properties, and linear algebra.

Exercise and practical sessions + 2 lectures. 75h

Static analysis of programs with complex data-structures for improvement of scheduling strategies at compile-time. When compiling, data structures are very hard to optimize. In fact, we have solutions only for affine programs working on arrays. It is called polyhedral compilation. But real world programs use various kinds of data structures. The goal is to find general methods to find all dependancies in a code kernel using complex data structures, such that recursive structures (e.g. trees).

Static Analysis of security properties in critical embedded software. Some software are called "critical" meaning that any fail would be grievous. To ensures safety of this kind of software, we use sound methods to mathematically be sure that the code can't cause any runtime error. In my case, I work on Airbus software to prove some properties about low level security, e.g., memory isolation. For this purpose, I am currently developing the support of x86 in Astrée analyser. http://www.astree.ens.fr/

Proof of the absence of runtime error in the codepage library "libiconv" (C language) using Frama-C, a static analyser using abstract interpretation. Development of frama-clang, a Frama-C plugin which allows it to analyse programs in C++. It works by compiling C++ into internal representation of C programs. This way, all methods developped for C works as well on C++. https://trust-in-soft.com/ https://frama-c.com/frama-clang.html

Oral Examiner in Mathematics in "Aux Lazaristes" CPGE, Lyon, FR CPGE are intensive preparatory classes to the entrance exam toFrench “Grande Écoles”

Proving the security of software-intensive embedded systems by abstract interpretation. To ensure safety of critical source code, we use abstract interpretation. This method is well known for some kind of languages. But when we mix different languages, analyzing them can become difficult. In industrial code, we find a mix of C and assembly, extremely entangled. While they are traditionnaly analyzed in different ways, I'm working on a almighty method to analyze both these languages at once.

Obtained with highest honors

Theoretical Computer Science.

Theoretical Computer Science.