Weakest precondition semantics for time and concurrency

DOI10.1016/0020-0190(92)90116-DzbMath0769.68086OpenAlexW1981930797MaRDI QIDQ1195491

H. S. M. Zedan, David Scholefield

Publication date: 29 November 1992

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(92)90116-d

zbMATH Keywords

verificationformal semanticsreal-time systemsrefinement calculusconcurrencypredicate transformersreal-time concurrent languageweakest precondition semantics

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55)

Related Items (6)

A specification-oriented semantics for the refinement of real-time systems ⋮ Transformational vs reactive refinement in real-time systems ⋮ A theory of Orwellian specifications with NewThink ⋮ Automatic generation of path conditions for concurrent timed systems ⋮ Weakest precondition semantics for time and concurrency ⋮ Real-time refinement in Manna and Pnueli's temporal logic

Cites Work

• A theoretical basis for stepwise refinement and the programming calculus
• Weakest precondition semantics for time and concurrency
• Real-time refinement in Manna and Pnueli's temporal logic
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item

This page was built for publication: Weakest precondition semantics for time and concurrency