A Framework for Certified Self-Stabilization

DOI10.1007/978-3-319-39570-8_3zbMath1347.68358arXiv1610.08685OpenAlexW4301524813MaRDI QIDQ2827460

Stéphane Devismes, Karine Altisen, Pierre Corbineau

Publication date: 19 October 2016

Published in: Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1610.08685

zbMATH Keywords

potential functionsself-stabilizationproof assistantCoqsilent algorithms

Mathematics Subject Classification ID

Related Items (4)

Certification of an exact worst-case self-stabilization time ⋮ Why3-do: the way of harmonious distributed system proofs ⋮ Squeezing streams and composition of self-stabilizing algorithms ⋮ Synchronous gathering without multiplicity detection: a certified algorithm

Uses Software

• Coq
• CoLoR

Cites Work

• Competitive self-stabilizing \(k\)-clustering
• Impossibility of gathering, a certification
• How to write a 21\(^{\text{st}}\) century proof
• A self-stabilizing algorithm for constructing spanning trees
• Self-stabilizing depth-first token circulation on networks
• Formal Verification of Distributed Algorithms
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Proving termination with multiset orderings
• Self-stabilizing systems in spite of distributed control

This page was built for publication: A Framework for Certified Self-Stabilization