Weak second order characterizations of various program verification systems

DOI10.1016/0304-3975(89)90156-4zbMath0678.68008OpenAlexW1991123457MaRDI QIDQ1124311

Ildikó Sain, Johann A. Makowsky

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)90156-4

zbMATH Keywords

comprehension schemesecond order logicProgram verification

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Recursive programs and denotational semantics in absolute logics of programs, Temporal logics need their clocks, On the strength of temporal proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Total correctness in nonstandard logics of programs
• A completeness theorem for dynamic logic
• A simple proof for the completeness of Floyd's method
• Non-standard algorithmic and dynamic logic
• 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
• On universal algebraic constructions of logics
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• The contributions of Alfred Tarski to algebraic logic
• Syntax directed analysis of liveness properties of while programs
• On folk theorems
• Ten Years of Hoare's Logic: A Survey—Part I