Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101837
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:07:38 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:08 AM

File

RR2002-14.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101837, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

10

Files downloads

38