Formal Justification of a Proof System for Communicating Sequential Processes

DOI10.1145/322358.322372MaRDI QIDQ3969859zbMATH OpenOpenAlexWikidataFDO

Authors 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

cooperating proofsCSPlogics of programsoperational semanticspartial correctnessrelative completenesssoundnesstotal correctness

Mathematics Subject Classification ID

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

Cited in

(12)

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

This page was built for publication: Formal Justification of a Proof System for Communicating Sequential Processes

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