inria-00099561, version 1
Correction de conjectures fausses par synthèse de programmes
Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003 - JFPLC'2003 (2003) 4 p
Abstract: 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.
- a – UR URPAH, FACULTE DES SCIENCES DE TUNIS, DSI
- b – UNIVERSITE HENRI POINCARE
- 1:
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Other
- Keywords : correction predicates – program synthesis || prédicats de correction – synthèse de programmes
- Internal note : A03-R-218 || demba03a
- Comment : Colloque avec actes et comité de lecture. internationale.
- inria-00099561, version 1
- http://hal.inria.fr/inria-00099561
- oai:hal.inria.fr:inria-00099561
- From:
- Submitted on: Tuesday, 26 September 2006 09:38:42
- Updated on: Wednesday, 10 January 2007 16:52:26
Export