- [[Safety]]および[[Liveness]]の初出論文 # 書誌情報 - **タイトル**: Proving liveness properties of concurrent programs - **著者**: Owicki, Susan,Lamport, Leslie - **出版年**: 1982 - **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. # 論文 - [Proving the Correctness of Multiprocess Programs](https://lamport.azurewebsites.net/pubs/proving.pdf)