%0 Conference Proceedings
%T Formal Analysis of a Distributed Algorithm for Tracking Progress
%+ Microsoft Research Silicon Valley
%+ University of California (UC)
%A Abadi, Martín
%A Mcsherry, Frank
%A Murray, Derek, G.
%A Rodeheffer, Thomas, L.
%Z Part 2: Session 1: Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Florence, Italy
%Y Dirk Beyer
%Y Michele Boreale
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7892
%P 5-19
%8 2013-06-03
%D 2013
%R 10.1007/978-3-642-38592-6_2
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Tracking the progress of computations can be both important and delicate in distributed systems. In a recent distributed algorithm for this purpose, each processor maintains a delayed view of the pending work, which is represented in terms of points in virtual time. This paper presents a formal specification of that algorithm in the temporal logic TLA, and describes a mechanically verified correctness proof of its main properties.
%G English
%2 https://inria.hal.science/hal-01515239/document
%2 https://inria.hal.science/hal-01515239/file/978-3-642-38592-6_2_Chapter.pdf
%L hal-01515239
%U https://inria.hal.science/hal-01515239
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-7892
%~ IFIP-FMOODS