A Proof System for Communicating Sequential Processes
From MaRDI portal
Publication:3922144
DOI10.1145/357103.357110zbMath0468.68023OpenAlexW1984831616MaRDI QIDQ3922144
No author found.
Publication date: 1980
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://ir.cwi.nl/pub/10267
blockingCSPconcurrencyglobal invariantpartial correctnesscooperating proofsabsence of deadlockHoare-style proof rules
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items
An axiomatic semantics for nested concurrency ⋮ Total correctness of CSP programs ⋮ Reasoning about dynamically evolving process structures ⋮ Transformations for communication fairness in CSP ⋮ A principle for sequential reasoning about distributed algorithms ⋮ Communication in concurrent dynamic logic ⋮ Deadlock analysis in networks of communicating processes ⋮ Interleaving set temporal logic ⋮ The laws of Occam programming ⋮ A proof system for distributed processes ⋮ Semantics and verification of monitors and systems of monitors and processes ⋮ A proof system for asynchronously communicating deterministic processes ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Semantics of nondeterminism, concurrency, and communication ⋮ Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems ⋮ On the use of history variables ⋮ A proof technique for communicating sequential processes ⋮ Issues in the design of a parallel object-oriented language ⋮ A system for compositional verification of asynchronous objects ⋮ Verification of object-oriented programs: a transformational approach ⋮ Verifying atomic data types ⋮ Deadlock-freedom in component systems with architectural constraints ⋮ Proof theory for exception handling in a tasking environment ⋮ Compositional Verification for Component-Based Systems and Application ⋮ Towards a foundation for semantics in complete metric spaces ⋮ Safety assurance via on-line monitoring ⋮ Design and verification of fault tolerant systems with CSP ⋮ The Automatic Detection of Token Structures and Invariants Using SAT Checking ⋮ A class of systems with nearly zero distributed simulation overhead ⋮ Efficient distributed simulation of acyclic systems ⋮ Verification of distributed programs using representative interleaving sequences ⋮ Using Hoare Logic in a Process Algebra Setting ⋮ A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs ⋮ An assertion-based proof system for multithreaded Java ⋮ A Bibliography of Willem-Paul de Roever ⋮ A Small Step for Mankind ⋮ Reasoning about Recursive Processes in Shared-Variable Concurrency ⋮ A Proof System for a PGAS Language ⋮ A brief history of process algebra ⋮ The pursuit of deadlock freedom ⋮ Semantic specification and verification of data flow diagrams ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Models and logics for true concurrency. ⋮ Logical models of discrete even systems: a comparative exposition ⋮ Fifty years of Hoare's logic ⋮ Mitigating Multi-target Attacks in Hash-Based Signatures ⋮ A shared-variable concurrency analysis of multi-threaded object-oriented programs ⋮ Corrigenda:Cooperating proofs for distributed programs with multiparty interactions ⋮ P-A logic - a compositional proof system for distributed programs ⋮ Correctness proofs of CSP programs ⋮ AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗ ⋮ A weakest precondition semantics for communicating processes ⋮ A proof outline logic for object-oriented programming ⋮ Distributed automata in an assumption-commitment framework ⋮ On the suitability of trace semantics for modular proofs of communicating processes ⋮ Specification-oriented semantics for communicating processes ⋮ A complete axiomatic semantics of spawning ⋮ Computation of equilibria in noncooperative games
