Mechanically verifying the fundamental liveness property of the Chord protocol

DOI10.1007/978-3-030-30942-8_5MaRDI QIDQ6535942zbMATH OpenFDO

Authors Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_5

zbMATH Keywords

Chorddistributed protocollivenessparameterized verificationstabilization proof

Mathematics Subject Classification ID

Network protocols (68M12) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Proving properties of the Chord protocol using the ASM formalism
• Re-Chord: a self-stabilizing chord overlay network
• On "A Simple Protocol Whose Proof Isńt": The State Machine Approach
• Algorithms – ESA 2005
• Liveness of randomised parameterised systems under arbitrary schedulers

Cites work

• Active and Concurrent Topology Maintenance
• Analysis of the evolution of peer-to-peer systems
• Proving properties of the Chord protocol using the ASM formalism

This page was built for publication: Mechanically verifying the fundamental liveness property of the Chord protocol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535942)