A calculus of total correctness for communicating processes

DOI10.1016/0167-6423(81)90005-8zbMath0485.68025OpenAlexW2128645239MaRDI QIDQ1164413

C. A. R. Hoare

Publication date: 1981

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:311bdad9-0361-4fd4-b7f1-388701f008bf

zbMATH Keywords

conditionalnondeterminismalternationassertionmutual recursionbuffering protocolschannel renamingdisjoint parallelismintended behaviournamed channelsprocess chainingsimple recursion

Mathematics Subject Classification ID

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

Related Items

Testing equivalences for processes, Computational models for networks of tiny artifacts: a survey, Correctness of concurrent processes, The equivalence in the DCP model, A process algebraic view of input/output automata, Specification and automatic verification of self-timed queues, A note on specifying and verifying concurrent processes, Algebraic characterizations of trace and decorated trace equivalences over tree-like structures, P-A logic - a compositional proof system for distributed programs, A more complete model of communicating processes, A linear-history semantics for languages for distributed programming, Strong fairness and full abstraction for communicating processes, On the suitability of trace semantics for modular proofs of communicating processes, Specification-oriented semantics for communicating processes