Verification of distributed programs using representative interleaving sequences

DOI10.1007/BF02252682zbMath0773.68053OpenAlexW1990161286MaRDI QIDQ1200917

Shmuel Katz, Doron A. Peled

Publication date: 16 January 1993

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02252682

zbMATH Keywords

partial order semanticsdistributed programscommunication-closed layersinterleaving setproof lattices

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Continuous lattices and posets, applications (06B35) Distributed algorithms (68W15)

Related Items

Detecting causal relationships in distributed computations: In search of the holy grail ⋮ Combining static analysis and case-based search space partitioning for reducing peak memory in model checking ⋮ An application of temporal projection to interleaving concurrency ⋮ On projective and separable properties ⋮ Adding partial orders to linear temporal logic ⋮ A pragmatic approach to stateful partial order reduction ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ On equivalence-completions of fairness assumptions ⋮ On stubborn sets in the verification of linear time temporal properties ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ Proving partial order properties

Cites Work

• Event fairness and non-interleaving concurrency
• Decomposition of distributed programs into communication-closed layers
• Defining liveness
• Appraising fairness in languages for distributed programming
• Alternative semantics for temporal logics
• Interleaving set temporal logic
• A proof rule for fair termination of guarded commands
• “Sometimes” and “not never” revisited
• A Proof System for Communicating Sequential Processes
• Proving Liveness Properties of Concurrent Programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Communicating sequential processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verification of distributed programs using representative interleaving sequences