Total correctness in nonstandard logics of programs

DOI10.1016/0304-3975(87)90118-6MaRDI QIDQ580955zbMATH OpenOpenAlexFDO

Authors 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

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)

Recommendations

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

Cites work

• scientific article; zbMATH DE number 3839296 (Why is no real title available?)
• scientific article; zbMATH DE number 3900134 (Why is no real title available?)
• scientific article; zbMATH DE number 3924132 (Why is no real title available?)
• scientific article; zbMATH DE number 3979058 (Why is no real title available?)
• scientific article; zbMATH DE number 3703966 (Why is no real title available?)
• scientific article; zbMATH DE number 3755858 (Why is no real title available?)
• scientific article; zbMATH DE number 3776849 (Why is no real title available?)
• scientific article; zbMATH DE number 3777465 (Why is no real title available?)
• scientific article; zbMATH DE number 3782362 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 3628347 (Why is no real title available?)
• scientific article; zbMATH DE number 3999893 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A complete logic for reasoning about programs via nonstandard model theory. II
• A completeness theorem for dynamic logic
• A simple dynamic logic
• A simple proof for the completeness of Floyd's method
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Is “sometime” sometimes better than “always”?
• Non-standard algorithmic and dynamic logic
• On the termination of program schemas
• Programs and program verifications in a general setting
• Recursive Programs as Definitions in First-Order Logic
• STRUCTURED NONSTANDARD DYNAMIC LOGIC

Cited in

(15)

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

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)