A New Incompleteness Result for Hoare's System

DOI10.1145/322047.322062MaRDI QIDQ4139636zbMATH OpenOpenAlexFDO

Authors Mitchell Wand

Publication date 1978

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/322047.322062

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Cited in

(21)

• Proving program inclusion using Hoare's logic
• On the completeness of modular proof systems
• Generating algebraic laws from imperative programs
• On the mechanical derivation of loop invariants
• The semantics of Hoare's iteration rule
• A methodology for designing proof rules for fair parallel programs
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Average case optimality for linear problems
• Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
• Some questions about expressiveness and relative completeness in Hoare's logic
• Fifty years of Hoare's logic
• Weakly expressive models for Hoare logic
• Semantical analysis of specification logic
• Recursive assertions are not enough - or are they?
• Proof methods of declarative properties of definite programs
• scientific article; zbMATH DE number 3688675 (Why is no real title available?)
• Current methods for proving program correctness
• Some general incompleteness results for partial correctness logics
• A language independent proof of the soundness and completeness of generalized Hoare logic
• Expressiveness and the completeness of Hoare's logic
• A mechanical analysis of program verification strategies

This page was built for publication: A New Incompleteness Result for Hoare's System

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