The ``Hoare Logic of CSP, and All That

DOI10.1145/2993.357247zbMath0536.68017OpenAlexW2123464354MaRDI QIDQ3321433

Fred B. Schneider, Leslie Lamport

Publication date: 1984

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/1813/6330

zbMATH Keywords

noninterferencesafety propertiesmessage-passingcommunicating sequential processesdecomposition principlecooperation proofsgeneralized Hoare logicinvariance properties of programs

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Related Items

Gordon's computer: A hardware verification case study in OBJ3 ⋮ Local Symmetry and Compositional Verification ⋮ A proof system for distributed processes ⋮ Atomic semantics of nonatomic programs ⋮ A language independent proof of the soundness and completeness of generalized Hoare logic ⋮ Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Wait-free linearization with an assertional proof ⋮ Reasoning about programs by exploiting the environment ⋮ A criterion for atomicity ⋮ Time and logic: A calculus of binary events ⋮ Defining liveness

This page was built for publication: The ``Hoare Logic of CSP, and All That