Formal verification of a programming logic for a distributed programming language

DOI10.1016/S0304-3975(97)00234-XMaRDI QIDQ1285659zbMATH OpenOpenAlexFDO

Authors Cui Zhang, Ronald A. Olsson, Karl Levitt

Publication date 28 April 1999

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

Full work available at URL https://doi.org/10.1016/s0304-3975(97)00234-x

zbMATH Keywords

semantic formalizationdistributed programming languagesmachine-checked verificationmechanization of programming logics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 1706329
• Publication:4733386
• Verification of distributed programs of the SPMD-type on the basis of the \(L\)-programs formalism
• Formal Verification of Distributed Algorithms

Cites work

• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 53100 (Why is no real title available?)
• scientific article; zbMATH DE number 108539 (Why is no real title available?)
• scientific article; zbMATH DE number 108540 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Automatic program verification. I: A logical basis and its implementation
• Axiomatic semantics of communicating sequential processes
• Logic and Computation
• The existence of refinement mappings

Cited in

(7)

• Language-oriented formal analysis: a case study on protocols and distributed systems
• scientific article; zbMATH DE number 4201637 (Why is no real title available?)
• Formal Verification of Distributed Algorithms
• Verifying distributed systems: the operational approach
• scientific article; zbMATH DE number 5713654 (Why is no real title available?)
• A proof system for distributed processes
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

Describes a project that uses

Uses Software

• ML
• HOL
• UNITY
• Cambridge LCF

This page was built for publication: Formal verification of a programming logic for a distributed programming language

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