Proving Liveness Properties of Concurrent Programs

346Citations
Citations of this article
109Readers
Mendeley users who have this article in their library.

Abstract

A liveness property asserts that program execution eventually reaches some desirable state. While termination has been studied extensively, many other liveness properties are important for concurrent programs. A formal proof method, based on temporal logic, for deriving liveness properties is presented. It allows a rigorous formulation of simple informal arguments. How to reason with temporal logic and how to use safety (invariance) properties in proving liveness is shown. The method is illustrated using, first, a simple programming language without synchronization primitives, then one with semaphores. However, it is applicable to any programming language. © 1982, ACM. All rights reserved.

Cite

CITATION STYLE

APA

Owicki, S., & Lamport, L. (1982). Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(3), 455–495. https://doi.org/10.1145/357172.357178

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free