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
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101837
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:07:38 AM
Last modification on : Thursday, November 21, 2019 - 2:38:41 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

5

Files downloads

14