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

DOI10.1305/NDJFL/1093635239zbMATH Open0696.03013OpenAlexW1972583224MaRDI QIDQ910396FDOQ910396

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

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
• Logical analysis of demonic nondeterministic programs

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)

Cited In (6)

• Inductive completeness of logics of programs
• Strong Semantical Characterization for Nondeterministic Programs
• Total correctness in nonstandard logics of programs
• On the Completeness of Dynamic Logic
• Title not available (Why is that?)
• On the strength of temporal proofs

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)