Non-standard algorithmic and dynamic logic

DOI10.1016/S0747-7171(86)80013-XzbMath0594.68032MaRDI QIDQ1077159

Ana Pasztor

Publication date: 1986

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

surveyformal programnon-standard dynamic logicpartial and total correctness of programsverification methods

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Nonstandard models (03H99)

Related Items (8)

Does “N+1 times” prove more programs correct than “N times”? ⋮ 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 ⋮ Semantical analysis of specification logic ⋮ Total correctness in nonstandard logics of programs ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ On the strength of temporal proofs

Cites Work

• The temporal semantics of concurrent programs
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• First-order dynamic logic
• Arithmetical interpretations of dynamic logic
• On the strength of “sometimes” and “always” in program verification
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• The complexity of the validity problem for dynamic logic
• A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
• Ten Years of Hoare's Logic: A Survey—Part I
• On the termination of program schemas
• Is “sometime” sometimes better than “always”?
• Soundness and Completeness of an Axiom System for Program Verification
• Some independence results for Peano arithmetic
• An axiomatic basis for computer programming
• Completeness in the theory of types
• 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
• 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: Non-standard algorithmic and dynamic logic