Lamport, Leslie; Schneider, Fred B.
We present a theorem for deriving properties of a concurrent program by reasoning about a simpler, coarser-grained version. The theorem generalizes a result that Lipton proved for partial correctness and deadlock-freedom. Our theorem applies to all safety properties.
computer science; technical report
Previously Published As