Internship

Master Internship #3: Static Analysis by Abstract Interpretation: Collecting Types of Python Programs

From March to August 2018, I worked under the supervision of Antoine Miné at the LIP6 laboratory, in Paris, France. I designed a static analysis by abstract interpretation that detects potential type errors in Python programs. I implemented this analysis into a modular static analyzer called MOPSA. You can find my report here, and my slides here.

Master Internship #2: Formal Verification of a Static Analyzer

From February to June 2017, I worked under the supervision of Eva Darulova at the Max Planck Institute for Software Systems (MPI-SWS), in Saarbrücken, Germany. I worked on a static analyser of floating-point programs called Daisy. I extended the formal verification of Daisy, to provide support for mixed-precision floating-point arithmetic. This formal verification consisted in a certificate checker, written in Coq and HOL4. You can find my report here, and my slides here.

Master Internship #1: Black-box Variational Inference in Probabilistic Programs

From May to July 2016, I worked with Hongseok Yang at the University of Oxford, United Kingdom, on “Variational Inference in Probabilistic Programs”. During this internship, we expressed probabilistic programming languages into probabilistic transition systems. Then, we developed a new variational inference algorithm working on a probabilistic transition system. You can find my report here, and my slides here (but in French).

Bachelor Internship: BATMAN, a BAsic Thread-Modular ANalyzer

From June to July 2015, I worked under the supervision of Antoine Miné at the École Normale Supérieure, France, on static analysis by abstract interpretation of concurrent programs. I learned how to use the Abstract Interpretation framework to develop, implement and test new methods to analyze concurrent programs more precisely. I implemented a prototype in OCaml, using the Apron library, and compared the results obtained with this approach to an academic analyzer called Concurinterproc.