Mechanical Verification of Concurrent Systems with TLA. - Urban Engberg; Peter Grønning; Leslie Lamport (CAV, 1992)