Correctness proofs of distributed termination algorithms

DOI10.1145/5956.6000MaRDI QIDQ3735060zbMATH OpenOpenAlexFDO

Authors Krzysztof R. Apt

Publication date 1986

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://www.acm.org/pubs/contents/journals/toplas/1986-8/

zbMATH Keywords

CSPdeadlockglobal invariantliveness properties of temporal logicweak total correctness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• scientific article; zbMATH DE number 3926219
• A distributed algorithm for distributed termination
• scientific article; zbMATH DE number 3903951
• Distributed algorithms for static and dynamic termination detection
• scientific article; zbMATH DE number 3938558
• Verification by construction of distributed algorithms
• scientific article; zbMATH DE number 222692
• scientific article; zbMATH DE number 2016070

Cited in

(10)

• Two normal form theorems for CSP programs
• A fully distributed termination detection scheme
• Fifty years of Hoare's logic
• A construction of distributed reference counting
• A compositional framework for fault tolerance by specification transformation
• An assertional proof of Rana's algorithm
• Design and verification of fault tolerant systems with CSP
• Comments on ``On the proof of a distributed algorithm: Always-true is not invariant
• scientific article; zbMATH DE number 3926219 (Why is no real title available?)
• Application of three-valued logic for distributed termination detection

This page was built for publication: Correctness proofs of distributed termination algorithms

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