Distributed Algorithms: A Challenging Playground for Model Checking (Invited Talk)

Author Nathalie Bertrand

Thumbnail PDF


  • Filesize: 317 kB
  • 1 pages

Document Identifiers

Author Details

Nathalie Bertrand
  • Univ Rennes, Inria, CNRS, IRISA, France

Cite AsGet BibTex

Nathalie Bertrand. Distributed Algorithms: A Challenging Playground for Model Checking (Invited Talk). In 25th International Conference on Principles of Distributed Systems (OPODIS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 217, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Distributed computing is increasingly spreading, in advanced technological applications as well as in our daily life. Failures in distributed algorithms can have important human and financial consequences, so that is is crucial to develop rigorous techniques to verify their correctness. Model checking is a model-based approach to formal verification, dating back the 80’s. It has been successfully applied first to hardware, and later to software verification. Distributed computing raises new challenges for the model checking community, and calls for the development of new verification techniques and tools. In particular, the parameterized verification paradigm is nowadays blooming to help proving automatically the correctness of distributed algorithms. In this invited talk, we present recent parameterized verification developments to automatically prove properties of some classical distributed algorithms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Distributed algorithms
  • Verification
  • Distributed algorithms


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail