The Hoare logic of concurrent programs

DOI10.1007/BF00289062MaRDI QIDQ754637zbMATH OpenOpenAlexFDO

Authors Leslie Lamport

Publication date 1980

Published in Acta Informatica (Search for Journal in Brave)

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

zbMATH Keywords

concurrent programscorrectnessHoare logicPnueli's temporal logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Cites work

• An axiomatic basis for computer programming
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Proving assertions about parallel programs

Cited in

(12)

• The lifeness property of on-the-fly garbage collector - a proof
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• A language independent proof of the soundness and completeness of generalized Hoare logic
• Correctness of substring-preprocessing in Boyer-Moore's pattern matching algorithm
• Invariants, composition, and substitution
• Méthode axiomatique sur les propriétés de fatalité des programmes parallèles
• Reasoning about programs by exploiting the environment
• Wait-free linearization with an assertional proof
• On using temporal logic for refinement and compositional verification of concurrent systems
• The autonomous data language -- concepts, design and formal verification
• Probabilistic predicate transformers. II: Partially observable probability
• Concurrent IMP

This page was built for publication: The Hoare logic of concurrent programs

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