On the completeness of propositional Hoare logic

DOI10.1016/S0020-0255(01)00164-5MaRDI QIDQ1602554zbMATH OpenOpenAlexDBLPWikidataFDO

Authors 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, https://hdl.handle.net/1813/7420

zbMATH Keywords

completenessexpressivenesspropositional Hoare logic

Mathematics Subject Classification ID

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

Recommendations

• Expressiveness and the completeness of Hoare's logic
• scientific article; zbMATH DE number 2110620
• Some questions about expressiveness and relative completeness in Hoare's logic
• Two theorems about the completeness of Hoare's logic
• scientific article; zbMATH DE number 3860376

Cites work

• Floyd-Hoare logic in iteration theories
• scientific article; zbMATH DE number 4055578 (Why is no real title available?)
• scientific article; zbMATH DE number 3737019 (Why is no real title available?)
• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 1142324 (Why is no real title available?)
• scientific article; zbMATH DE number 1142325 (Why is no real title available?)
• Program correctness and matricial iteration theories
• Propositional dynamic logic of regular programs
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(27)

• Some questions about expressiveness and relative completeness in Hoare's logic
• A language independent proof of the soundness and completeness of generalized Hoare logic
• The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
• Equational theories for automata
• Fifty years of Hoare's logic
• Deciding Kleene algebra terms equivalence in Coq
• A genetically modified Hoare logic
• Completeness of Hoare logic relative to the standard model
• Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
• Equational theories of abnormal termination based on Kleene algebra
• Partial derivative automata formalized in Coq
• Unified Classical Logic Completeness
• scientific article; zbMATH DE number 3848602 (Why is no real title available?)
• On the Meaning of Logical Completeness
• scientific article; zbMATH DE number 3639591 (Why is no real title available?)
• scientific article; zbMATH DE number 1512073 (Why is no real title available?)
• Proving completeness by logic
• scientific article; zbMATH DE number 2110620 (Why is no real title available?)
• Some Completeness Results for Propositional Conditional Logics
• Semantic Foundations for Deterministic Dataflow and Stream Processing
• The Hoare logic of deterministic and nondeterministic monadic recursion schemes
• A note on the complexity of propositional Hoare logic
• First order Büchi automata and their application to verification of LTL specifications
• Alignment complete relational Hoare logics for some and all
• Correctly compiling proofs about programs without proving compilers correct
• Expressiveness and the completeness of Hoare's logic
• Completeness of Hoare logic with inputs over the standard model

This page was built for publication: On the completeness of propositional Hoare logic

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