Weakest preconditions for progress

DOI10.1007/BF01212336zbMATH Open0753.68068OpenAlexW2101027003MaRDI QIDQ1189258FDOQ1189258

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

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

zbMATH Keywords

weakest preconditionsprogress properties

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Properties of a predicate transformer of the VRS system

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)