Mathematiques A Raisonnement E Logiciel L E

in English

Accueil. Equipe Logiciels. Stages. Rapport d´activité Actions AOC , Concert Séminaire. Bibliographie

Vérification sur ordinateurs de démonstrations et de logiciels. L'objectif du projet Marelle est d'étudier l'utilisation de techniques de vérification de démonstration sur ordinateur pour assurer la correction de logiciel. Les domaines visés sont les logiciels de calcul scientifique (calcul formel, arithmétiques des ordinateurs). le projet développe des méthodes et des outils pour aider à produire des programmes corrects à partir de descriptions précises des données, des algorithmes ainsi qu'à partir de leurs propriétés et des preuves de ces propriétés. Axes de recherche: Environnements de preuves Formalisation des mathématiques et théorie des types Algorithmique certifiée Propriétés formelles des nombres, calcul exact. collaborations scientifiques: types working group: raisonnement assité par ordinateur fondé sur la théorie des types. Actions de recherche coopératives: AOC (Arithmétique des ordinateurs certifiée), Concert Projet Mowgli (projet européen LTR): mathématiques formelles sur le Web (Universités de Bologne, de Berlin, de Nijmgen et Eindhoven, DFKI Saarbrücken, Max Planck Institute, et Trusted Logic) Université de Nice, laboratoire A.Dieudonné: formalisation des shémas en géométrie algébrique. Domaines d'application potentiels: Vérification formelle des aspects suivants: logiciel controlant des dispositifs physiques (transport, robotique médicale, contrôle d'attitude de satellites), compilateurs pour des langages spécialisés, précision de calculs à base de nombres flottants, probabilités d'erreur dans les logiciels.

Contact: Yves.Bertot@sophia.inria.fr