HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formal Verification Of Pastry Using TLA+

Tianxiang Lu 1, 2 Stephan Merz 1, 3, 4 Christoph Weidenbach 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available, but to the best of our knowledge the correctness of the algorithm has not been verified formally. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, we believe that it makes an interesting target for verification using TLA+. More precisely, our goal is to model the join and lookup protocols of Pastry using the TLA+ language, and to use the associated tools to verify significant correctness properties.
Document type :
Conference papers
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, December 24, 2012 - 11:43:56 AM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM
Long-term archiving on: : Monday, March 25, 2013 - 3:50:33 AM


Files produced by the author(s)


  • HAL Id : hal-00768812, version 1



Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Formal Verification Of Pastry Using TLA+. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France. ⟨hal-00768812⟩



Record views


Files downloads