# AFormal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

 Title: A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm Authors: Ben Fiedler (ben /dot/ fiedler /at/ inf /dot/ ethz /dot/ ch) and Dmitriy Traytel Submission date: 2020-07-21 Abstract: We provide a suitable distributed system model and implementation of the Chandy--Lamport distributed snapshot algorithm [ACM Transactions on Computer Systems, 3, 63-75, 1985]. Our main result is a formal termination and correctness proof of the Chandy--Lamport algorithm and its use in stable property detection. BibTeX: @article{Chandy_Lamport-AFP, author = {Ben Fiedler and Dmitriy Traytel}, title = {A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm}, journal = {Archive of Formal Proofs}, month = jul, year = 2020, note = {\url{https://isa-afp.org/entries/Chandy_Lamport.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Ordered_Resolution_Prover