MOPSA
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.
An informal introduction to Abstract Interpretation on Patrick Cousot's web page (in English 
). Patrick Cousot is a co-inventor with Radhia Cousot of Abstract Interpretation.
Watch also the video by Patrick Cousot at Collège de France (in French 
).
An article about the MOPSA project on the CNRS website (in French ).