Completeness of Hoare logic with inputs over the standard model

DOI10.1016/J.TCS.2015.08.004MaRDI QIDQ896915zbMATH OpenOpenAlexFDO

Authors Zhaowei Xu, Yuefei Sui, Wenhui Zhang

Publication date 15 December 2015

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

Full work available at URL https://doi.org/10.1016/j.tcs.2015.08.004

zbMATH Keywords

computationPeano arithmeticstandard modelHoare logicarithmetical definabilitylogical completeness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) First-order arithmetic and fragments (03F30)

Recommendations

• Completeness of Hoare logic relative to the standard model
• Expressiveness and the completeness of Hoare's logic
• Two theorems about the completeness of Hoare's logic
• On relative completeness of Hoare logics
• On the completeness of propositional Hoare logic

Cites work

• scientific article; zbMATH DE number 51556 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• An axiomatic basis for computer programming
• Computability and Logic
• Expressiveness and the completeness of Hoare's logic
• Hoare's logic and Peano's arithmetic
• On the completeness of propositional Hoare logic
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(3)

• First order Büchi automata and their application to verification of LTL specifications
• The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
• Completeness of Hoare logic relative to the standard model

This page was built for publication: Completeness of Hoare logic with inputs over the standard model

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