On the strength of “sometimes” and “always” in program verification

DOI10.1016/S0019-9958(83)80042-4zbMath0549.68019OpenAlexW2047004999MaRDI QIDQ3341880

László Csirmaz

Publication date: 1983

Published in: Information and Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0019-9958(83)80042-4

zbMATH Keywords

loop invariantsalwaysnonstandard dynamic logicsometimestime quantifiers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (3)

Non-standard algorithmic and dynamic logic ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach

This page was built for publication: On the strength of “sometimes” and “always” in program verification