Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Résumé : Nous présentons une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe. Cet algorithme exécute une seule passe sur le graphe le parcourant en profondeur d'abord. Notre programme est ici écrit dans un style de programmation fonctionnelle dans le langage Why3-ML. La preuve utilise des lemmes et des assertions exprimés dans la logique de Why3. La majorité d'entre eux sont prouvés automatiquement à l'exception de 5 assertions ou lemmes prouvés manuellement en Coq. Une preuve d'une version impérative de ce programme ne figure pas dans ce travail, mais nous indiquons comment y parvenir par raffinements successifs. Un point important est que nos preuves sont intuitives, publiables et lisibles par un humain.
https://hal.inria.fr/hal-01422227 Contributor : Jean-Jacques LevyConnect in order to contact the contributor Submitted on : Saturday, December 24, 2016 - 10:59:18 AM Last modification on : Wednesday, June 15, 2022 - 3:48:20 AM Long-term archiving on: : Saturday, March 25, 2017 - 12:30:20 PM
Jean-Jacques Levy, Ran Chen. Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm. Groupe de travail LTP du GDR GPL , Nov 2016, Orsay, France. 2016. ⟨hal-01422227⟩