A weakest precondition semantics for communicating processes

DOI10.1016/0304-3975(84)90001-XzbMath0532.68035MaRDI QIDQ789174

Nissim Francez, Tzilla Elrad

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

terminationnondeterminismdistributed programmingdeadlock

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A linear-history semantics for languages for distributed programming
• Extended naming conventions for communicating processes
• Semantics of nondeterminism, concurrency, and communication
• A calculus of communicating systems
• The programming language Ada. Reference manual. Proposed standard document, United States Department of Defense
• Deadlock absence proofs for networks of communicating processes
• A proof technique for communicating sequential processes
• An axiomatic proof technique for parallel programs
• Formal derivation of strongly correct concurrent programs
• A Proof System for Communicating Sequential Processes
• Communicating sequential processes
• Distributed processes
• Concurrent Processes and Their Syntax
• High level programming for distributed computing
• Programming as a Discipline of Mathematical Nature

This page was built for publication: A weakest precondition semantics for communicating processes