Other Relevant Work

Last modified 16 April 2018
This page contains links to pages outside the TLA+ and TLAPS web sites that are related to TLA.  Most of the sites listed are old, and there are undoubtedly more recent sites that should be here.  If you'd like links to your work added to this page, contact us.
Large Scale Model Checking 101
This is a video by Markus Kuppe giving practical advice on using the TLC model checker for checking large models. Dated April 11, 2018.

A TLA+ Workshop
These are the slides of talks and the submitted papers from a TLA+ workshop that was held in Paris on 27 August 2012 in conjunction with the FM 2012 conference.

Stephan Merz
A page containing several papers on TLA by Stephan Merz, as well as a link to Isabelle/TLA, Merz's encoding of TLA in the higher-order logic of the generic interactive theorem prover Isabelle.  (That page includes a machine-checked proof of The Dagstuhl RPC-Memory Example.)

Work With and On Lamport's TLA .
Publications by the Networks and Distributed Systems group at the University of Bielefeld, headed by Peter Ladkin.  They are all dated 1996 and 1997, but at least some of them are still worth reading.

Tools for TLA based specifications
This page describes work done in the early 1990s at the University of Dortmund, Department of Computer Science by the Computer Networks and Distributed Systems group headed by Dr. Heiko Krumm.