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

DOI10.1007/BF02311231MaRDI QIDQ757079zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A compositional proof system for distributed programs
• scientific article; zbMATH DE number 4201637
• A proof system for distributed processes
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes
• Proof rules for fault tolerant distributed programs

Cites work

• scientific article; zbMATH DE number 3903940 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• A Proof System for Communicating Sequential Processes
• A calculus of total correctness for communicating processes
• A proof method for cyclic programs
• A proof technique for communicating sequential processes
• Communicating sequential processes
• Correctness proofs of CSP programs
• Defining liveness
• Proofs of Networks of Processes
• Total correctness of CSP programs

Cited in

(18)

• Proof rules for fault tolerant distributed programs
• Programming Languages and Systems
• An explanatory presentation of composition rules for assumption- commitment specifications
• A Logic For Distributed Processes
• scientific article; zbMATH DE number 4201637 (Why is no real title available?)
• An introduction to compositional methods for concurrency and their application to real-time.
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts
• Distributed automata in an assumption-commitment framework
• Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
• A compositional proof system for distributed programs
• A proof system for distributed processes
• scientific article; zbMATH DE number 3997153 (Why is no real title available?)
• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• Modular verification of multithreaded programs
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Logical foundations for compositional verification and development of concurrent programs in UNITY
• A trace-based compositional proof theory for fault tolerant distributed systems
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes

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

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