Some general incompleteness results for partial correctness logics
From MaRDI portal
Publication:1110500
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
program verificationincompleteness theoremsHoare logicscalculus of partial correctness proofs of programs
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
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
