An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic

DOI10.1305/NDJFL/1093635239MaRDI QIDQ910396zbMATHOpenAlexFDO

Authors Ildikó Sain

Publication date 1989

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1093635239

zbMATH Keywords

semanticssecond-order logicFloyd-Hoare logicnondeterministic programsrelational tracestime-models

Mathematics Subject Classification ID

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

Recommendations

• Strong Semantical Characterization for Nondeterministic Programs
• scientific article; zbMATH DE number 3921949
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• scientific article; zbMATH DE number 4200180
• Logical analysis of demonic nondeterministic programs

Cited in

(6)

• Total correctness in nonstandard logics of programs
• On the Completeness of Dynamic Logic
• Strong Semantical Characterization for Nondeterministic Programs
• On the strength of temporal proofs
• Inductive completeness of logics of programs
• scientific article; zbMATH DE number 3921949 (Why is no real title available?)

This page was built for publication: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic

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