Squeezing streams and composition of self-stabilizing algorithms
From MaRDI portal
Publication:6190178
DOI10.1007/978-3-030-21759-4_2OpenAlexW2949031189MaRDI QIDQ6190178
Pierre Corbineau, Stéphane Devismes, Karine Altisen
Publication date: 6 February 2024
Published in: Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-21759-4_2
Distributed algorithms (68W15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Competitive self-stabilizing \(k\)-clustering
- A self-stabilizing \(k\)-clustering algorithm for weighted graphs
- How to write a 21\(^{\text{st}}\) century proof
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Coinductive big-step operational semantics
- Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
- Formal verification of mobile robot protocols
- A Framework for Certified Self-Stabilization
- Formal Verification of Distributed Algorithms
- Copatterns
- Self-stabilizing systems in spite of distributed control
- Mechanizing coinduction and corecursion in higher-order logic
- An application of co-inductive types in Coq: Verification of the alternating bit protocol
- An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
- Model Checking of a Mobile Robots Perpetual Exploration Algorithm
- Typed Lambda Calculi and Applications
This page was built for publication: Squeezing streams and composition of self-stabilizing algorithms