On the completeness of propositional Hoare logic

DOI10.1016/S0020-0255(01)00164-5zbMath0996.03022OpenAlexW2029498583WikidataQ61634976 ScholiaQ61634976MaRDI QIDQ1602554

Dexter Kozen, Jerzy Tiuryn

Publication date: 23 June 2002

Published in: Information Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0020-0255(01)00164-5

zbMATH Keywords

completenessexpressivenesspropositional Hoare logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ A genetically modified Hoare logic ⋮ Completeness of Hoare logic with inputs over the standard model ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra ⋮ Fifty years of Hoare's logic ⋮ Partial Derivative Automata Formalized in Coq ⋮ Equational theories for automata ⋮ Deciding Kleene algebra terms equivalence in Coq

Cites Work

• Propositional dynamic logic of regular programs
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Floyd-Hoare logic in iteration theories
• Program correctness and matricial iteration theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item