License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.DISC.2023.2
URN: urn:nbn:de:0030-drops-191284
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19128/
Go to the corresponding LIPIcs Volume Portal

Altisen, Karine ; Corbineau, Pierre ; Devismes, Stéphane

Certified Round Complexity of Self-Stabilizing Algorithms

pdf-format:
LIPIcs-DISC-2023-2.pdf (0.9 MB)

Abstract

A proof assistant is an appropriate tool to write sound proofs. The need of such tools in distributed computing grows over the years due to the scientific progress that leads algorithmic designers to consider always more difficult problems. In that spirit, the PADEC Coq library has been developed to certify self-stabilizing algorithms. Efficiency of self-stabilizing algorithms is mainly evaluated by comparing their stabilization times in rounds, the time unit that is primarily used in the self-stabilizing area. In this paper, we introduce the notion of rounds in the PADEC library together with several formal tools to help the certification of the complexity analysis of self-stabilizing algorithms. We validate our approach by certifying the stabilization time in rounds of the classical Dolev et al’s self-stabilizing Breadth-first Search spanning tree construction.

BibTeX - Entry

@InProceedings{altisen_et_al:LIPIcs.DISC.2023.2,
  author =	{Altisen, Karine and Corbineau, Pierre and Devismes, St\'{e}phane},
  title =	{{Certified Round Complexity of Self-Stabilizing Algorithms}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{2:1--2:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19128},
  URN =		{urn:nbn:de:0030-drops-191284},
  doi =		{10.4230/LIPIcs.DISC.2023.2},
  annote =	{Keywords: Certification, proof assistant, Coq, self-stabilization, round complexity}
}

Keywords: Certification, proof assistant, Coq, self-stabilization, round complexity
Collection: 37th International Symposium on Distributed Computing (DISC 2023)
Issue Date: 2023
Date of publication: 05.10.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI