L'objectif est de concevoir une formalisation de l'arithmétique réelle adaptée à l'assistant de preuves Coq et utilisable dans le cadre de la vérification formelle de programmes numériques. L'accent sera mis sur les méthodes modernes de preuve et la facilité d'utilisation de la bibliothèque.
Context
La vérification formelle d'un logiciel passe par des formalisations permettant de spécifier ce que le programme doit faire (correction) ou ne pas faire (sûreté), ainsi que des méthodes automatiques permettant de garantir que c'est bien le cas. L'assistant de preuve Coq est un cadre globalement adapté pour effectuer des preuves déductives de programme. Mais pour ce qui est des programmes numériques, sa formalisation démodée des nombres réels et le manque d'automatisations associées constituent en fait un frein à leur vérification.
Objectives
L'objectif de ce projet est de revisiter la bibliothèque des réels de Coq au vu des nombreuses avancées dans ce domaine, afin de fixer des bases et des outils adaptés à la preuve de programmes numériques. La thèse s'intéresse aux bases d'une bonne formalisation.
Work program
Extra information
Demande de financement soumise au DIM LSC (projet Coquelicot)
Prerequisite
Détails
Expected funding
Research contract
Status of funding
Confirmed
Candidates
Catherine Lelay, M2 Logique Mathématique et Fondements de l'Informatique, Université Paris 7
Utilisateur
sylvie.boldo
Créé
Vendredi 29 avril 2011 13:40:39 CEST
dernière modif.
Mardi 17 mai 2011 15:09:39 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit Assistante
Stéphanie Druetta Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr