Hoare's logic for nondeterministic regular programs: A nonstandard approach
From MaRDI portal
Publication:1822934
DOI10.1016/0304-3975(89)90165-5zbMath0679.68024MaRDI 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
03B60: Other nonclassical logic
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68N01: General topics in the theory of software
Related Items
Total correctness in nonstandard logics of programs, Weak second order characterizations of various program verification systems
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
