P-A logic - a compositional proof system for distributed programs

DOI10.1007/BF02311231zbMath0723.68075OpenAlexW2039277865MaRDI QIDQ757079

Paritosh K. Pandya, Mathai Joseph

Publication date: 1991

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02311231

zbMATH Keywords

proof systemSafetylifenessOCCAM

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Related Items (9)

Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency ⋮ Theory and methodology of assumption/commitment based system interface specification and architectural contracts ⋮ Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ A foundation for modular reasoning about safety and progress properties of state-based concurrent programs ⋮ Modular verification of multithreaded programs ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Distributed automata in an assumption-commitment framework ⋮ An explanatory presentation of composition rules for assumption- commitment specifications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Defining liveness
• Total correctness of CSP programs
• A proof technique for communicating sequential processes
• A calculus of total correctness for communicating processes
• A proof method for cyclic programs
• Correctness proofs of CSP programs
• A Proof System for Communicating Sequential Processes
• Proofs of Networks of Processes
• Communicating sequential processes

This page was built for publication: P-A logic - a compositional proof system for distributed programs