A simple proof for the completeness of Floyd's method

DOI10.1016/0304-3975(85)90024-6zbMath0552.68003OpenAlexW2007789697MaRDI QIDQ801661

Ildikó Sain

Publication date: 1985

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

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

zbMATH Keywords

first order logiccompleteness of Floyd's methodprogram verification methodssemantics for programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10)

Related Items (8)

Recursive programs and denotational semantics in absolute logics of programs ⋮ Weak second order characterizations of various program verification systems ⋮ Total correctness in nonstandard logics of programs ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ Stability of weak second-order semantics ⋮ Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs? ⋮ Program correctness on finite fields ⋮ On the strength of temporal proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting

This page was built for publication: A simple proof for the completeness of Floyd's method