The Hoare logic of concurrent programs

DOI10.1007/BF00289062zbMATH Open0416.68032OpenAlexW1983409972MaRDI QIDQ754637FDOQ754637

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

Hoare logiccorrectnessconcurrent programsPnueli'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

• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Proving assertions about parallel programs

Cited In (9)

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

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)