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

DOI10.1016/S0019-9958(83)80042-4MaRDI QIDQ3341880zbMATH OpenOpenAlexFDO

Authors 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

alwaysloop invariantsnonstandard dynamic logicsometimestime quantifiers

Mathematics Subject Classification ID

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

Recommendations

• A vindication of program verification
• scientific article; zbMATH DE number 3907752
• scientific article; zbMATH DE number 1390248
• Program analysis is harder than verification: a computability perspective
• Program verification as probabilistic inference

Cited in

(8)

• Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• Non-standard algorithmic and dynamic logic
• Comments on Always-true is not invariant: Assertional reasoning about invariance
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs?
• Recursive programs and denotational semantics in absolute logics of programs
• Does “N+1 times” prove more programs correct than “N times”?
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

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

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