Formal communication elimination and sequentialization equivalence proofs for distributed system models

DOI10.1007/S00236-014-0203-0MaRDI QIDQ466919zbMATH OpenOpenAlexFDO

Authors Miquel Bertran, Francesc Babot, August Climent

Publication date 31 October 2014

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00236-014-0203-0

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Distributed systems (68M14)

Recommendations

• Formal sequentialization of distributed systems via program rewriting
• An input/output semantics for distributed program equivalence reasoning
• scientific article; zbMATH DE number 1832216
• Verification of distributed programs using representative interleaving sequences
• scientific article; zbMATH DE number 1059321

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 43800 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 53772 (Why is no real title available?)
• scientific article; zbMATH DE number 177253 (Why is no real title available?)
• scientific article; zbMATH DE number 1487860 (Why is no real title available?)
• scientific article; zbMATH DE number 1487866 (Why is no real title available?)
• scientific article; zbMATH DE number 1746645 (Why is no real title available?)
• scientific article; zbMATH DE number 1832216 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A calculus of communicating systems
• Algebra of communicating processes with abstraction
• An input/output semantics for distributed program equivalence reasoning
• Concurrency verification. Introduction to compositional and noncompositional methods
• Consolidated Ada reference manual. Language and standard libraries. International standard ISO/ IEC 8652/1995(E) with technical corrigendum 1
• Data Refinement
• Decomposition of distributed programs into communication-closed layers
• Distributed cooperation with action systems
• Formal sequentialization of distributed systems via program rewriting
• Partial-order reduction in symbolic state-space exploration
• Prespecification in data refinement
• Process algebra for synchronous communication
• Proof of correctness of data representations
• Refinement Calculus
• Refinement of fair action systems
• Static analysis for state-space reductions preserving temporal logics
• Temporal verification of reactive systems: response
• The laws of Occam programming

Cited in

(3)

• An input/output semantics for distributed program equivalence reasoning
• Formal sequentialization of distributed systems via program rewriting
• scientific article; zbMATH DE number 7724201 (Why is no real title available?)

Describes a project that uses

Uses Software

• PVS
• Ada95

This page was built for publication: Formal communication elimination and sequentialization equivalence proofs for distributed system models

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