Defining liveness
Information Processing LettersPublished 1 October 1985
Bowen Alpern, Fred B. Schneider
Citations1,025
SJR quartileQ3
SJR score0.41
SNIP0.73
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A formal definition for liveness properties is proposed, and every property is shown to be the intersection of a safety property and a liveness property.
Abstract
A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that 'something good' eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.
Keywords
Computer Science
IEEE Transactions on Software EngineeringProving the Correctness of Multiprocess Programs
1,101 Citations1977Leslie Lamport
The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs, represented by ordinary flowcharts, and no special synchronization mechanisms are assumed.
ACM Transactions on Programming Languages and SystemsProving Liveness Properties of Concurrent Programs
583 Citations1982Susan Owicki, Leslie Lamport
A formal proof method, based on temporal logic, for deriving liveness properties is presented, which allows a rigorous formulation of simple informal arguments and how to reason with temporal logic and use safety (invariance) properties in proving liveness is shown.
Lecture notes in computer sciencePower domains and predicate transformers: A topological view
229 Citations2006Michael Smyth
The specific tasks are to provide a more adequate framework for power-domain constructions; and to show that the connection between (Dijkstra's) weakest preconditions and the Smyth powerdomain, established by Plotkin for the case of flat domains, actually holds in full generality.
ACM Transactions on Programming Languages and SystemsThe ``Hoare Logic'' of CSP, and All That
116 Citations1984Leslie Lamport, Fred B. Schneider
A simple meta-rule of the generalized Hoare logic-the decomposition principle-is described, showing how all these methods for reasoning about concurrent programs can be derived using it.
On characterization of safety and liveness properties in temporal logic
47 Citations1985A. Prasad Sistla