My advisor is Antoine Miné and my topic is abstract interpretation under relaxed memory models.
My main research interest is the use of formal methods to ensure the security, safety and correctness of programs. I am particularly interested in static analysis by the means of abstract interpretation of programs to automatically and soundly ensure properties of programs such as the absence of some classes of errors.
I am also occasionnally interested in strong and expressive type systems and programming languages that use them, programming language implementation, and binary code analysis.
Abstract. We address the verification problem of numeric properties in many-threaded concurrent programs under weakly consistent memory models, especially TSO. We build on previous work that proposed an abstract interpretation method to analyse these programs with relational domains. This method was not sufficient to analyse more than two threads in a decent time. Our contribution here is to rely on a rely-guarantee framework with automatic inference of thread interferences to design an analysis with a thread-modular approach and describe relational abstractions of both thread states and interferences. We show how to adapt the usual computing procedure of interferences to the additional issues raised by weakly consistent memories. We demonstrate the precision and the performance of our method on a few examples, operating a prototype analyser that verifies safety properties like mutual exclusion. We discuss how weak memory models affect the scalability results compared to a sequentially consistent environment.
Abstract. We address the problem of verifying concurrent programs under store-buffer-based weakly consistent memory models, such as TSO or PSO. Using the abstract interpretation framework, we adapt existing domains for arrays to model store buffers and obtain a sound abstraction of program states (including the case of programs with infinite state space) parameterised by a numerical domain. Whereas the usual method for this kind of programs implements a program transformation to come back to an analysis under a sequentially consistent model, the novelty of our work consists in applying abstract interpretation directly on the source program, setting a clean foundation for special dedicated domains keeping information difficult to express with program transformations. We demonstrate the precision of this method on a few examples, targetting the TSO model and incidentally being also sound for PSO due to some specific abstraction choice. We discuss an application to fence removal and show that our implementation is usually able to remove as many or more fences, with respect to the state of the art, on concurrent algorithms designed for sequential consistency while still remaining precise enough to verify them.
Here is some software I maintain or contributed to.
An experimental static analyser for concurrent programs within relaxed memory models.
A graph library for OCaml. I implemented the WeakTopological and ChaoticIteration modules for fixpoint computation using widening.
A LaTeX to HTML translator. During my internship in the Gallium team, I reworked the output module with ropes and authored the HTML5 generator.
I have been a teaching assistant in the following courses.
Feel free to send me an email to my personal address . I also currently use the address but it will become inactive at some point.Équipe Antique