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.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.