Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Abstract : 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.
https://hal.inria.fr/hal-01515239 Contributor : Hal IfipConnect in order to contact the contributor Submitted on : Thursday, April 27, 2017 - 10:46:45 AM Last modification on : Thursday, July 25, 2019 - 3:06:02 PM Long-term archiving on: : Friday, July 28, 2017 - 12:39:26 PM
Martín Abadi, Frank Mcsherry, Derek G. Murray, Thomas L. Rodeheffer. Formal Analysis of a Distributed Algorithm for Tracking Progress. 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), Jun 2013, Florence, Italy. pp.5-19, ⟨10.1007/978-3-642-38592-6_2⟩. ⟨hal-01515239⟩