@inproceedings{lamport2002specifying,
author = {Lamport, Leslie and Matthews, John and Tuttle, Mark and Yu, Yuan},
title = {Specifying and verifying systems with TLA+},
organization = {INRIA (Institut National de Recherche en Informatique et en Automatique)},
booktitle = {Proceedings of the Tenth ACM SIGOPS European Workshop},
year = {2002},
month = {September},
abstract = {TLA+ is a high-level specification language that has been used to specify and check the correctness of several hardware protocols. We expect that it can also be used to specify and check concurrent algorithms and protocols for software systems.

This describes our experience at DEC/Compaq using TLA+ and the TLC model checker on several systems, mainly cache-coherence protocols. It is shorter than, and more up-to-date than [128].},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/specifying-and-verifying-systems-with-tla/},
pages = {45-48},
edition = {Proceedings of the Tenth ACM SIGOPS European Workshop},
}