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. The prototype is available on Github.

You can find my report here, and my slides here (but in French) This internship lead to a publication in VMCAI’17.