The MOPSA research project aims at developing effective methods and tools to make computer software more reliable.
MOPSA is a software verification project grounded in formal methods. Such methods employ mathematical and logical tools to reason on programs, providing rigorous correctness guarantees. The project focuses on developing static analyses, i.e., tools able to automatically infer properties of program executions at compile-time and thus detect whole classes of software defects. The project leverages the theory of abstract interpretation to design analyses that are approximate, in order to scale up to large programs, and sound, so that no program behavior is overlooked during the analysis (achieving full control and data coverage and providing a high confidence in the analysis results).
Static analysis methods have enjoyed a growing success, at least for specialized applications, as witnessed for instance by the commercial release of industrial tools such as the Astrée analyzer that proves the absence of run-time errors in embedded C code. The MOPSA project aims at improving the theory and design of static analyzers and broadening their application to the general software development community. Planned research topics include: developing novel modular abstractions to analyze software one component at a time and improve scalability without sacrificing precision, targeting more dynamic languages (such as Python) that have recently become more popular, and inferring novel program properties beyond safety that may prove useful to help the continuous development and deployment of software (e.g., portability analyses and patch effect analyses).
The project will develop an open-source, extensible static analysis platform to showcase our research results and help disseminating static analysis techniques.
MOPSA is funded by the European Research Council through a Consolidator ERC Grant from 2016 to 2021.
The project is hosted at LIP6, a joint laboratory of Sorbonne Université and CNRS in Paris, France.
The MOPSA project is looking to hire motivated PhD candidates and post-docs.
The PhD candidate should have a strong background in formal software verification and static analysis by Abstract Interpretation, and good programming skills. The candidate should have followed a Master-level course in program analysis at least similar in scope and contents as the following courses: at MPRI (English), at ENS, (English), or at Sorbonne Université (French). PhD positions are 3-year long (which is the legal duration in France).
The ideal post-doc candidate should have a PhD in formal verification of software, preferably related to static analysis and Abstract Interpretation, and some experience in implementing formal verification tools. Post-doc positions are 1-year, renewable,
For information and application, please contact:
Watch also the video by Patrick Cousot at Collège de France (in French ).