Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2002

Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq

Résumé

The firing squad synchronization is a cellular automata problem introduced by Moore; in 1987, J.Mazoyer gave a six state solution to this problem. The proof of correctness of this solution uses discrete geometrical considerations, but is quite hard to verify due to the multiplication of cases and indexes. To be more confident in this proof, a proof assistant developed by the Inria, Coq has been used. This report exposes the development in Coq of this proof. A large use of inductive structures, a natural way in Coq, offers a clearer vision of the Mazoyer's solution. The full development of the proof is avalaible in the contributions of the Coq software.
La synchronisation d’une ligne de fusiliers est un problème d’automates cellulaires posé par Moore, en 1987, J.Mazoyer donna une solution avec six états à ce problème. La preuve de correction de cette solution utilise des considérations de géométrie discrète, mais elle est assez difficile à vérifier à cause de la multiplication des cas et des indices. Pour être plus sûr de cette preuve, un assistant à la preuve développé par l’Inria, Coq, a été utilisé. Ce rapport expose le développement en Coq de la preuve. Un grand usage des structures inductives, une voie naturelle en Coq, offre une vision plus claire de la solution de J.Mazoyer. Le développement complet de la preuve est disponible dans les contributions du logiciel Coq
Fichier principal
Vignette du fichier
RR2002-14.pdf (354.68 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101837 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101837 , version 1

Citer

Jean Duprat. Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq. [Research Report] LIP RR-2002-14, Laboratoire de l'informatique du parallélisme. 2002, 2+36p. ⟨hal-02101837⟩
21 Consultations
70 Téléchargements

Partager

Gmail Facebook X LinkedIn More