A complete logic for reasoning about programs via nonstandard model theory. II
From MaRDI portal
Publication:1159461
DOI10.1016/0304-3975(82)90025-1zbMath0475.68010OpenAlexW4256371891MaRDI QIDQ1159461
Ildikó Sain, Hajnalka Andréka, Istvan Németi
Publication date: 1982
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(82)90025-1
Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Nonstandard models (03H99)
Related Items (17)
Non-standard algorithmic and dynamic logic ⋮ A simple dynamic logic ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ Some general incompleteness results for partial correctness logics ⋮ Weak second order characterizations of various program verification systems ⋮ Output concepts for accelerated Turing machines ⋮ Temporal logics need their clocks ⋮ Axiomatizing fixpoint logics ⋮ Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics ⋮ On strictly arithmetical completeness in logics of programs ⋮ Total correctness in nonstandard logics of programs ⋮ A unifying theorem for algebraic semantics and dynamic logics ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ A simple proof for the completeness of Floyd's method ⋮ Some questions about expressiveness and relative completeness in Hoare's logic ⋮ On the strength of temporal proofs ⋮ An essay in combinatory dynamic logic
Cites Work
- A theory of interactive programming
- Programs and program verifications in a general setting
- Model theory
- Model theory for tense logics
- On the termination of program schemas
- Soundness and Completeness of an Axiom System for Program Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A complete logic for reasoning about programs via nonstandard model theory. II
