E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, 1999.

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003.
DOI : 10.1109/32.588521

L. Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, vol.5, issue.1, pp.1-11, 1987.
DOI : 10.1145/7351.7352
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.226.5361

L. Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

L. Lamport, Checking a Multithreaded Algorithm with ???+???CAL, 20th Intl. Symp. Distributed Computing, pp.151-163, 2006.
DOI : 10.1007/11864219_11

Y. Yu, P. Manolios, and L. Lamport, Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of LNCS, pp.54-66, 1999.
DOI : 10.1007/3-540-48153-2_6