An assertional proof of Rana's algorithm

DOI10.1016/0020-0190(94)90059-0MaRDI QIDQ1318748zbMATH OpenOpenAlexFDO

Authors Michiel C. van Wezel, Gerard Tel

Publication date 5 April 1994

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(94)90059-0

zbMATH Keywords

distributed computingprogram correctnesssafetylivenesscorrectness prooftermination detection algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• Correctness proofs of distributed termination algorithms
• scientific article; zbMATH DE number 3926219
• Comments on ``On the proof of a distributed algorithm: Always-true is not invariant
• A mechanical proof of Segall's PIF algorithm
• Distributed termination detection for dynamic systems

Cites work

• A distributed solution of the distributed termination problem
• An assertional correctness proof of a distributed algorithm
• Derivation of a termination detection algorithm for distributed computations
• Distributed termination detection for dynamic systems
• Self-stabilizing extensions for message-passing systems
• Time, clocks, and the ordering of events in a distributed system

Cited in

(5)

• scientific article; zbMATH DE number 2080213 (Why is no real title available?)
• scientific article; zbMATH DE number 512976 (Why is no real title available?)
• Two blossoming proofs of the Lane-Riesenfeld algorithm
• scientific article; zbMATH DE number 3926219 (Why is no real title available?)
• A short proof of an algorithm by Boehm

This page was built for publication: An assertional proof of Rana's algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1318748)