Alexis Pocquet

Curriculum

Research Experience

• Bachelor Research Internship
  CNRS, ENS Paris, Antique team - Jérôme Féret and Jérôme Boillot - may 2025 to july 2025

  During my first internship with the Antique team at ENS Paris, under the supervision of Jérôme Féret and Jérôme Boillot, I discovered Abstract Interpretation and its application to operating system formal verification. [...] In this work, I proposed a method to verify that operating system properties are preserved during the execution of application tasks on the IA-32 architecture by introducing an intermediate language with a formal semantics to model assembly instructions. From this, I derived a semantics characterizing all states reachable during task execution and constructed a sound and sufficiently precise over-approximation of reachability analysis based on constraint-manipulating functions over memory states. This approach makes it possible to compute memory states corresponding to writes in critical regions, and I defined a set of states that I proved to be stable under this abstract analysis, provided that application executions do not compromise the integrity of the host system’s essential data structures.

• Bachelor Research Project
  CNRS, ENS Paris, Antique team - Jérôme Féret - january 2025 to may 2025

  During my sixth semester of bachelor, I discovered Abstract Interpretation and its applications to system software engineering at the Antique team of ENS Paris, under the supervision of Jérôme Féret, with a particular focus on several instantiations of the abstract notion of reduced product. [...] Abstract Interpretation, introduced by Patrick and Radhia Cousot in the late 1970s, formalizes program analysis as computations over over-approximations of reachable program states in order to ensure termination while retaining sufficient precision to infer meaningful invariants.
  
  Current research in Abstract Interpretation focuses on combining abstract domains to infer invariants of different natures within a single abstract interpreter, a construction known as a reduced product. My research project studied several instantiations of reduced products (such as those using input/output channels or ghost quantities) and analyzed how they address termination and refinement of abstract computations.

Programming

• KawaLang (winter 2025)
  

  Kawa is an object-oriented toy programming language developed for a third-year bachelor project as an introduction to applied programming language theory. The implementation, in OCaml, includes a basic interpreter and a static type checker designed for exhaustiveness and precise type error reporting. [...] The interpreter is quite naive and the pipeline for code execution is divided in three sequential parts : code parsing and structures loading, static type type-checking and code evaluation/execution. These two last phases strongly depend on symbol/name resolution, which is permanently being used during the interpretating process.
  
  This language should not be used for real projects since its implementation is experiemental and sometimes buggy. Here is a set of examples that I used to test my implementation.

I also enjoy some side projects, even if they are incomplete or not fully usable: C DeepSeek API (summer 2025) is an easy-to-use REST API in C for interacting with the DeepSeek API. Processor proto (spring 2022) is a C++ implementation of an abstract machine based on the Von Neumann architecture that interprets a simple assembly language. It is likely unstable, as I started it some time ago and haven’t updated it much since.