A calculus of total correctness for communicating processes

DOI10.1016/0167-6423(81)90005-8MaRDI QIDQ1164413zbMATH OpenOpenAlexFDO

Authors Tony 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

alternationassertionbuffering protocolschannel renamingconditionaldisjoint parallelismintended behaviourmutual recursionnamed channelsnondeterminismprocess chainingsimple recursion

Mathematics Subject Classification ID

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

Cited in

(14)

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

This page was built for publication: A calculus of total correctness for communicating processes

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