Hoare's logic for nondeterministic regular programs: A nonstandard approach
From MaRDI portal
Publication:1822934
DOI10.1016/0304-3975(89)90165-5zbMath0679.68024OpenAlexW2010093011MaRDI QIDQ1822934
M. Teresa Hortalá-González, Mario Rodríguez Artalejo
Publication date: 1989
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(89)90165-5
Other nonclassical logic (03B60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Related Items
Weak second order characterizations of various program verification systems ⋮ Total correctness in nonstandard logics of programs
Cites Work
- Total correctness in nonstandard logics of programs
- Proving program inclusion using Hoare's logic
- The axiomatic semantics of programs based on Hoare's logic
- A simple proof for the completeness of Floyd's method
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- Some questions about expressiveness and relative completeness in Hoare's logic
- Non-standard algorithmic and dynamic logic
- A simple dynamic logic
- Some general incompleteness results for partial correctness logics
- A complete logic for reasoning about programs via nonstandard model theory. II
- Programs and program verifications in a general setting
- First-order dynamic logic
- On the notion of expressiveness and the rule of adaptation
- On the strength of “sometimes” and “always” in program verification
- STRUCTURED NONSTANDARD DYNAMIC LOGIC
- A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
- Semantics of looping programs in Propositional Dynamic Logic
- Guarded commands, nondeterminacy and formal derivation of programs
- On the termination of program schemas
- Soundness and Completeness of an Axiom System for Program Verification
- Recursive Programs as Definitions in First-Order Logic
- Flow diagrams, turing machines and languages with only two formation rules
- An axiomatic basis for computer programming
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
