A Retrospective of <i>Proving the Correctness of Multiprocess Programs</i>

A historical perspective of a paper published in 1977. The major contribution of that paper was its informal definitions of safety and liveness properties. It provided a method for proving invariance (a safety property) that was equivalent to ones in several papers published at about the same time—the most influential being the Owicki-Gries method.