Mopsa est un logiciel de vérification de programmes 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. La démonstration présentera l’utilisation de Mopsa à travers quelques exemples simples en C et en Python. Elle mettra en évidence l’intérêt d’une conception modulaire en montrant comment, d’une part, un changement des abstractions utilisées permet d’éliminer des faux positifs et, d’autre part, comment une même abstraction est exploitée dans l’analyse de langages aussi différents que C et Python.