MOPSA analyzer : MOPSA Static Analyzer

Team : APR

MOPSA is a multi-language program verification software based on sound static analysis by abstract interpretation. It automatically infers invariants and detects, at compile time, the possible run-time errors. The analysis computes an interpretation of programs in a collection of reusable abstractions programmed in OCaml. Thanks to its modular conception, MOPSA can be easily extended in the set of properties and the set of analyzed languages. MOPSA currently supports significant subsets of the C and Python 3 languages. In C, MOPSA detects undefined behaviors as well invalid calls to the standard C library (specified in a dedicated modelization language). In Python, MOPSA, performs a type, value, and exception analysis.

Software leader : Antoine Miné
https://gitlab.com/mopsa/mopsa-analyzer