Aller au contenu Aller au menu Aller à la recherche

Vérification des programmes, fiabilité des logiciels, Mopsa, Antoine Miné

accès rapides, services personnalisés

Rechercher

Recherche détaillée

Egalement dans la rubrique

Contact

Direction de la communication

 

Marie Pinhas-Diena, responsable de la communication scientifique l T. 01 44 27 22 89 l M. marie.pinhas@upmc.fr

Vérification des programmes, fiabilité des logiciels, Mopsa, Antoine Miné

Les erreurs de programmation sont omniprésentes avec des conséquences allant de la frustration des utilisateurs à d’énormes pertes économiques ou humaines. Les méthodes de vérification des programmes sont coûteuses en temps et en expertise, c’est pourquoi seules les industries peuvent généralement les appliquer. Le projet ERC Mopsa d’Antoine Miné, professeur UPMC au laboratoire d’informatique de Paris 6 (LIP6, CNRS/UPMC), vise à simplifier cette démarche en élargissant les méthodes d’analyse statique par interprétation abstraite et en les intégrant dans une plate-forme open-source pour que tout développeur puisse vérifier son programme*.

 

© Frédéric Delvalle, LIP6

 

Le but de ses recherches est l'amélioration de la qualité et de la fiabilité des logiciels et des systèmes informatiques grâce à l'utilisation de méthodes formelles. Il conçoit des méthodes et des outils d'analyse statique capables de découvrir, automatiquement et dès la compilation, des propriétés des logiciels, par exemple l'absence de certains types d'erreurs. Ces méthodes sont fondées sur des sémantiques et donnent des garanties mathématiques rigoureuses concernant le fonctionnement des logiciels. Elles utilisent également des approximations permettant d'obtenir des analyses sûres en un temps raisonnable sur des logiciels réels. Ces méthodes sont conçues et prouvées sûres par interprétation abstraite, une théorie générale des approximations sûres de sémantiques.

 

Antoine Miné a travaillé sur les sujets suivants : les domaines abstraits numériques, l'analyse des calculs en virgule flottante, les modèles et les analyses de mémoire avec une sémantique de bas niveau, l'analyse de logiciels embarqués critiques, et l'analyse de logiciels multi-tâches.

Pour en savoir plus :

Laboratoire d’informatique de Paris 6 (LIP6, CNRS/UPMC) Nouvelle fenêtre

La page web d’Antoine MinéNouvelle fenêtre

 

* Source CNRS/INS2I.



20/04/16