Résumé
Vérifier que des systèmes informatiques ont le comportement attendu est une tâche complexe. L’expérience montre en effet que ces systèmes contiennent en général des erreurs plus ou moins critiques pour l'utilisateur et plus ou moins difficiles à corriger pour le concepteur. De nombreux travaux visent à proposer des formalismes spécialisés pour modéliser le système et le comportement souhaité ainsi que des méthodes et algorithmes pour réellement prouver son adéquation.
Plusieurs questions se posent alors sur la correction des méthodes proposées : a-t-on effectivement modélisé le bon programme et le bon comportement ? La méthode et son implantation sont-elles correctes ? Sont-elles suffisamment puissantes ? Ces questions ne sont pas seulement théoriques, car elles concernent directement les industriels qui développent des codes informatiques critiques et qui doivent garantir leur bon comportement en apportant suffisamment de justifications à l'organisme de certification.
In fine, notre conviction qu'une méthode est correcte repose sur une interprétation du problème en termes mathématiques et un raisonnement logique. Cependant, l'intrinsèque complexité des modèles mathématiques des programmes rend nécessaire un traitement informatisé de ces modèles.
À côté d'outils spécifiques à l'analyse de programmes s'est développée depuis les années 1970 une classe d'outils qui traitent des théories mathématiques générales. Les langages de description de théories et les formalismes de preuve varient suivant les systèmes.
Durant le séminaire, nous présenterons et motiverons plusieurs approches possibles (de la logique du premier ordre à la théorie des types). Nous illustrerons via l'exemple de l'assistant de preuve Coq, l'état de l'art de ce qui peut être réalisé actuellement en termes de mathématiques formalisées sur ordinateur.
