Correction de conjectures fausses par synthèse de programmes

Moussa Demba Francis Alexandre 1 Khaled Bsaïes
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Dans le domaine de la vérification, les preuves ne terminent pas toujours avec succès, à cause des formules non prouvables. Parfois, le prouveur signale simplement l'échec. Cependant, dans certains cas il est intéressant de connaître la cause de cet échec et de la corriger. Les méthodes classiques sont insuffisantes pour qu'un prouveur détecte et corrige automatiquement les incohérences dans les programmes ou les formules logiques. Dans cet article, nous proposons une méthode permettant de corriger de formules fausses. Soit $ \Phi(x)$ une formule fausse, la méthode présentée consiste à construire un prédicat de correction $P$ tel que $\forall x~(\Phi(x)\Leftarrow P(x))$ soit valide.
Type de document :
Communication dans un congrès
Ducassé, Mireille. Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003 - JFPLC'2003, 2003, Amiens, France, Lavoisier, 4 p, 2003
Liste complète des métadonnées

https://hal.inria.fr/inria-00099561
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:38:42
Dernière modification le : mardi 24 avril 2018 - 13:34:49

Identifiants

  • HAL Id : inria-00099561, version 1

Collections

Citation

Moussa Demba, Francis Alexandre, Khaled Bsaïes. Correction de conjectures fausses par synthèse de programmes. Ducassé, Mireille. Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003 - JFPLC'2003, 2003, Amiens, France, Lavoisier, 4 p, 2003. 〈inria-00099561〉

Partager

Métriques

Consultations de la notice

47