Formal Justification of a Proof System for Communicating Sequential Processes

DOI10.1145/322358.322372zbMath0503.68021OpenAlexW2060551365MaRDI QIDQ3969859

Krzysztof R. Apt

Publication date: 1983

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/322358.322372

zbMATH Keywords

operational semanticsCSPsoundnessrelative completenesspartial correctnesstotal correctnesslogics of programscooperating proofs

Mathematics Subject Classification ID

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

Related Items

Total correctness of CSP programs, The origins of structural operational semantics, Reasoning about dynamically evolving process structures, Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, Designing equivalent semantic models for process creation, A compositional proof system for distributed programs, Proof theory for exception handling in a tasking environment, A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs, Reasoning about Recursive Processes in Shared-Variable Concurrency, Fifty years of Hoare's logic, A shared-variable concurrency analysis of multi-threaded object-oriented programs, Specification-oriented semantics for communicating processes