Total correctness in nonstandard logics of programs

DOI10.1016/0304-3975(87)90118-6zbMATH Open0626.68008OpenAlexW2015731361MaRDI QIDQ580955FDOQ580955

Ildikó Sain

Publication date: 1987

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90118-6

Recommendations

• scientific article
• Non-standard algorithmic and dynamic logic
• scientific article; zbMATH DE number 4022609
• scientific article; zbMATH DE number 3921953
• Effective Axiomatizations of Hoare Logics

zbMATH Keywords

partial correctnessterminationintermittent assertions methodMann-Cooper method for proving total correctness assertions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• Non-standard algorithmic and dynamic logic
• A simple dynamic logic
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the termination of program schemas
• Is “sometime” sometimes better than “always”?
• Title not available (Why is that?)
• Title not available (Why is that?)
• Recursive Programs as Definitions in First-Order Logic
• A completeness theorem for dynamic logic
• A simple proof for the completeness of Floyd's method
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic

Cited In (15)

• Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics
• Semantical proofs of correctness for programs performing non-deterministic tests on real numbers
• Temporal logics need their clocks
• Title not available (Why is that?)
• Reasoning in Dynamic Logic about Program Termination
• Recursive programs and denotational semantics in absolute logics of programs
• Non-standard algorithmic and dynamic logic
• Algebraization of quantifier logics, an introductory overview
• General correctness: A unification of partial and total correctness
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unifying Recursion in Partial, Total and General Correctness
• Weak second order characterizations of various program verification systems
• On the strength of temporal proofs

This page was built for publication: Total correctness in nonstandard logics of programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q580955)