| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Prouvabilité et correction des formules implicatives
Résumé : Dans ce papier, nous proposons une méthode permettant d'étudier la prouvabilité des formules implicatives par analyse statique. Elle consiste à caractériser les formules et les programmes par des (in)équations mathématiques permettant de vérifier si une formule est satisfiable ou non sans effectuer le processus de preuve. Nous nous sommes aussi intéressés à la correction des formules fausses. En effet, nous proposons une méthode qui permet de synthétiser, pour une classe particulière de programmes et de formules implicatives, les prédicats de correction qui symbolisent les hypothèses manquantes à la formule pour qu'elle devienne vraie.
Cited literature [7 references]
https://hal.inria.fr/inria-00293706
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Monday, July 7, 2008 - 1:57:36 PM
Last modification on : Wednesday, October 28, 2020 - 2:20:03 PM
Long-term archiving on: : Friday, May 28, 2010 - 11:13:08 PM
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Monday, July 7, 2008 - 1:57:36 PM
Last modification on : Wednesday, October 28, 2020 - 2:20:03 PM
Long-term archiving on: : Friday, May 28, 2010 - 11:13:08 PM
File
pages-391-395-article24.pdf
Files produced by the author(s)