A proof technique for communicating sequential processes

DOI10.1007/BF00289266zbMath0463.68034MaRDI QIDQ1153686

David Gries, Gary Levin

Publication date: 1981

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

communicating sequential processesdeadlocktotal correctnessproof rules

Mathematics Subject Classification ID

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

Related Items

An axiomatic semantics for nested concurrency, Total correctness of CSP programs, A model and temporal proof system for networks of processes, A proof system for distributed processes, A compositional proof system for distributed programs, Axiomatic system for proving the properties of simple multimodule programs, Using Hoare Logic in a Process Algebra Setting, An assertion-based proof system for multithreaded Java, Auxiliary variables in partial correctness programming logics, An introduction to compositional methods for concurrency and their application to real-time., Fifty years of Hoare's logic, Corrigenda:Cooperating proofs for distributed programs with multiparty interactions, P-A logic - a compositional proof system for distributed programs, AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗, A weakest precondition semantics for communicating processes, Specification-oriented semantics for communicating processes, A complete axiomatic semantics of spawning, Computation of equilibria in noncooperative games

Cites Work

• Unnamed Item
• Unnamed Item
• Deadlock absence proofs for networks of communicating processes
• Assignment and Procedure Call Proof Rules
• A Proof System for Communicating Sequential Processes
• Distributed Termination
• Proofs of Networks of Processes
• Communicating sequential processes
• An axiomatic basis for computer programming