A compositional proof system for distributed programs

DOI10.1007/BFB0019365MaRDI QIDQ4560363zbMATH OpenFDO

Authors Kastytis Gečas

Publication date 11 December 2018

Published in Baltic Computer Science (Search for Journal in Brave)

zbMATH Keywords

operational semanticsproof systemtransition systemhistory variablememory state

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 4201637
• A proof system for distributed processes
• P-A logic - a compositional proof system for distributed programs
• scientific article; zbMATH DE number 3900140
• Axiomatic system for proving the properties of simple multimodule programs

Cites work

• scientific article; zbMATH DE number 3903940 (Why is no real title available?)
• scientific article; zbMATH DE number 3963180 (Why is no real title available?)
• A proof technique for communicating sequential processes
• An axiomatic basis for computer programming
• Axiomatic semantics of communicating sequential processes
• Communicating sequential processes
• Formal Justification of a Proof System for Communicating Sequential Processes
• Problem-oriented program verification
• Semantics of communication in simple multimodular programs
• Semantics of nondeterminism, concurrency, and communication
• Soundness and Completeness of an Axiom System for Program Verification

Cited in

(18)

• scientific article; zbMATH DE number 3997153 (Why is no real title available?)
• Distributed Computing
• An input/output semantics for distributed program equivalence reasoning
• Axiomatic system for proving the properties of simple multimodule programs
• scientific article; zbMATH DE number 3900139 (Why is no real title available?)
• Using message passing for distributed programming: proof rules and disciplines
• Causing communication closure: safe program composition with reliable non-FIFO channels
• scientific article; zbMATH DE number 3976314 (Why is no real title available?)
• A proof system for asynchronously communicating deterministic processes
• scientific article; zbMATH DE number 3900138 (Why is no real title available?)
• scientific article; zbMATH DE number 1533829 (Why is no real title available?)
• Programming Languages and Systems
• An experiment in program composition and proof
• Verification of distributed programs of the SPMD-type on the basis of the \(L\)-programs formalism
• A trace-based compositional proof theory for fault tolerant distributed systems
• scientific article; zbMATH DE number 4201637 (Why is no real title available?)
• scientific article; zbMATH DE number 3900140 (Why is no real title available?)
• Proof rules for fault tolerant distributed programs

This page was built for publication: 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 Q4560363)