Weakest preconditions for progress

DOI10.1007/BF01212336MaRDI QIDQ1189258zbMATH OpenOpenAlexFDO

Authors Johan J. Lukkien, Jan L. A. van de Snepscheut

Publication date 26 September 1992

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01212336

zbMATH Keywords

weakest preconditionsprogress properties

Mathematics Subject Classification ID

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

Recommendations

• A predicate transformer for progress
• A predicate transformer for the progress property `to-always'
• scientific article; zbMATH DE number 1531358
• Weakest precondition semantics for time and concurrency
• Safety and progress of recursive procedures

Cites work

• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Proving Liveness Properties of Concurrent Programs
• Temporal predicate transformers and fair termination

Cited in

(5)

• A predicate transformer for progress
• Weakest preconditions for pure Prolog programs
• Safety and progress of recursive procedures
• scientific article; zbMATH DE number 1531358 (Why is no real title available?)
• Properties of a predicate transformer of the VRS system

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: Weakest preconditions for progress

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