Weakly expressive models for Hoare logic
From MaRDI portal
Publication:805248
DOI10.1016/0304-3975(91)90232-QzbMath0728.68081MaRDI QIDQ805248
Publication date: 1991
Published in: Theoretical Computer Science (Search for Journal in Brave)
Other nonclassical logic (03B60) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Unnamed Item
- Unnamed Item
- Expressiveness and the completeness of Hoare's logic
- Hoare's logic for programming languages with two data types
- Some questions about expressiveness and relative completeness in Hoare's logic
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- Definability by programs in first-order structures
- Effective Axiomatizations of Hoare Logics
- A New Incompleteness Result for Hoare's System
- Soundness and Completeness of an Axiom System for Program Verification
- An axiomatic basis for computer programming