Completeness of Hoare logic with inputs over the standard model

DOI10.1016/J.TCS.2015.08.004zbMATH Open1333.68182OpenAlexW2187700024MaRDI QIDQ896915FDOQ896915

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Expressiveness and the completeness of Hoare's logic
• Computability and Logic
• Hoare's logic and Peano's arithmetic
• On the completeness of propositional Hoare logic

Cited In (3)

• Completeness of Hoare logic relative to the standard model
• 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

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)