Some general incompleteness results for partial correctness logics

DOI10.1016/0890-5401(88)90015-6zbMath0657.03011OpenAlexW2169088600MaRDI QIDQ1110500

Francisca Lucio-Carrasco, M. Teresa Hortalá-González, Mario Rodríguez Artalejo

Publication date: 1988

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(88)90015-6

zbMATH Keywords

program verificationincompleteness theoremsHoare logicscalculus of partial correctness proofs of programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Applications of computability and recursion theory (03D80) General topics in the theory of software (68N01)

Related Items

Hoare's logic for nondeterministic regular programs: A nonstandard approach

Cites Work

• Two theorems about the completeness of Hoare's logic
• Expressiveness and the completeness of Hoare's logic
• The axiomatic semantics of programs based on Hoare's logic
• Some questions about expressiveness and relative completeness in Hoare's logic
• Non-standard algorithmic and dynamic logic
• A complete logic for reasoning about programs via nonstandard model theory. II
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Recursive assertions are not enough - or are they?
• First-order dynamic logic
• Model theory
• On the notion of expressiveness and the rule of adaptation
• Recursive programs and denotational semantics in absolute logics of programs
• Gödel numberings of partial recursive functions
• The characterization problem for Hoare logics
• Ten Years of Hoare's Logic: A Survey—Part I
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• Another incompleteness result for Hoare's logic
• An axiomatic basis for computer programming
• Monadic Elementary Formal Systems
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Computability of Recursive Functions
• Elementary properties of Abelian groups
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item