Static analysis

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.

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.