MOPSA analyzer : Analyseur statique MOPSA

Équipe : APR

MOPSA est un logiciel de vérification de programmes multi-languages par analyse statique sûre basée sur la théorie de l'interprétation abstraite. Il infère automatiquement des invariants et détecte, à la compilation, les erreurs possibles à l'exécution. L'analyse calcule une interprétation des programmes dans une collection d'abstractions réutilisables et programmées en OCaml. Sa conception modulaire permet à MOPSA d'être extensible vis à vis des propriétés et des langages considérés. MOPSA supporte actuellement des sous-ensembles significatifs des langages C et Python 3. En C, MOPSA détecte les comportements indéfinis ainsi que l'utilisation invalide de la bibliothèque standard C (spécifiée dans un langage de modélisation dédié). En Python, MOPSA effectue une analyse de type, de valeur et des exceptions.

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