@inproceedings{yu1999model,
author = {Yu, Yuan and Manolios, Panagiotis and Lamport, Leslie},
title = {Model Checking TLA+ Specifications},
booktitle = {In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag.},
year = {1999},
month = {June},
abstract = {Despite my warning him that it would be impossible, Yuan Yu wrote a model checker for TLA+ specifications.  He succeeded beyond my most optimistic hopes.  This paper is a preliminary report on the model checker.  I was an author, at Yu's insistence, because I gave him some advice on the design of the model checker (more useful advice than just don't do it).  Manolios worked at SRC as a summer intern and contributed the state-compression algorithm that is described in the paper, but which ultimately was not used in the model checker.},
url = {http://approjects.co.za/?big=en-us/research/publication/model-checking-tla-specifications/},
pages = {54-66},
volume = {1703},
edition = {In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag.},
}