Dr. Marc Chevalier

Angestellt, Software Engineer, Snyk

Langnau am Albis, Switzerland

Skills

Software Development
C++
Rust (programming language)
Software Architecture
X86 assembly language
Python
teaching
Static code analysis
Ocaml
Formal methods
Software verification
Embedded Systems
Mathematics
LaTeX
Haskell
Bash (Unix shell)
LibreOffice
MS Office
Git
GitLab
GitHub
MatLab
Maple
Mathematica
Windows
Debian
Ubuntu
Formal Verification
Abstract Interpretation
Coq Theorem Prover

Timeline

Professional experience for Marc Chevalier

  • Current 3 years, since Apr 2021

    Software Engineer

    Snyk

    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.

  • 2 years and 9 months, Sep 2017 - May 2020

    Teacher of mathematics

    Centre Recherche Interdisciplinaire

    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.

  • 2 years and 9 months, Sep 2017 - May 2020

    Tutorial of Semantics Lecture

    École Normale Supérieure

    Exercise and practical sessions + 2 lectures. 75h

  • 6 months, Mar 2017 - Aug 2017

    Research Internship -- Compilers

    Ecole Normale Supérieure de Lyon

    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).

  • 7 months, Sep 2016 - Mar 2017

    Research Internship -- Program Analysis

    École Normale Supérieure de Paris

    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/

  • 3 months, May 2015 - Jul 2015

    R&D intern

    TrustinSoft

    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

  • 9 months, Sep 2014 - May 2015

    Oral Examiner

    Aux Lazaristes

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

Educational background for Marc Chevalier

  • 3 years and 3 months, Sep 2017 - Nov 2020

    PhD in Computer Science

    École Normale Supérieure

    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.

  • 11 months, Sep 2015 - Jul 2016

    MSc in Computer Science

    Ecole Polytechnique Fédérale de Lausanne EPFL

    Obtained with highest honors

  • 11 months, Sep 2014 - Jul 2015

    1st year of MSc in Computer Science

    Ecole Normale Superieure de Lyon

    Theoretical Computer Science.

  • 11 months, Sep 2013 - Jul 2014

    BSc. in Computer Science

    Ecole Normale Superieure de Lyon

    Theoretical Computer Science.

Languages

  • French

    First language

  • English

    Fluent

  • German

    Intermediate

  • Chinese

    Basic

Interests

Archery
Ski
Opera
Drama

Browse over 21 million XING members