TLA+ | The way to specify

Publications

The list of publications on TLA+, PlusCal, and the tools. Currently this list is under construction and is neither complete nor completely correct, and is missing a lot of information about these publications that will eventually appear here. If any of your publications are missing or listed incorrectly, please let us know.

• [2008,article] bibtex
  K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, "A TLA+ Proof System," CoRR, vol. abs/0811.1914, 2008.
  @article{DBLP_journals_corr_abs-0811-1914,
  author = {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz},
  title = {A TLA+ Proof System},
  journal = {CoRR},
  volume = {abs/0811.1914},
  year = {2008},
  ee = {http://arxiv.org/abs/0811.1914},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2008,proceedings] bibtex
  Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008CEUR-WS.org, 2008.
  @proceedings{DBLP_conf_lpar_2008w, editor = {Piotr Rudnicki and Geoff Sutcliffe and Boris Konev and Renate A. Schmidt and Stephan Schulz},
  title = {Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008},
  booktitle = {LPAR Workshops},
  publisher = {CEUR-WS.org},
  series = {CEUR Workshop Proceedings},
  volume = {418},
  year = {2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2008,inproceedings] bibtex
  K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, "A TLA+ Proof System," in LPAR Workshops, 2008.
  @inproceedings{DBLP_conf_lpar_ChaudhuriDLM08,
  author = {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz},
  title = {A TLA+ Proof System},
  booktitle = {LPAR Workshops},
  year = {2008},
  ee = {http://ceur-ws.org/Vol-418/paper2.pdf},
  crossref = {DBLP:conf/lpar/2008w},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2007,mastersthesis] bibtex
  N. Qutteineh, "Business Process Mediation Using TLA+," Master’s Dissertation , Hamburg, Germany, 2007.
  @mastersthesis{QUTTEINEH2007,
  author = {Nadeem Qutteineh},
  title = {Business Process Mediation Using TLA+},
  type = {Master Thesis},
  school = {Hamburg University of Technology},
  address = {Hamburg, Germany},
  month = Apr, year = {2007},
  }
• [2007,article] bibtex
  J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, "Formal specification of a Web services protocol," J. Log. Algebr. Program., vol. 70, iss. 1, pp. 34-52, 2007.
  @article{DBLP_journals_jlp_JohnsonLLV07,
  author = {James E. Johnson and David E. Langworthy and Leslie Lamport and Friedrich H. Vogt},
  title = {Formal specification of a Web services protocol},
  journal = {J. Log. Algebr. Program.},
  volume = {70},
  number = {1},
  year = {2007},
  pages = {34-52},
  ee = {http://dx.doi.org/10.1016/j.jlap.2006.05.004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,proceedings] bibtex
  Formal Techniques for Networked and Distributed Systems – FORTE 2006, 26th IFIP WG 6.1 International Conference, Paris, France, September 26-29, 2006Springer, 2006.
  @proceedings{DBLP_conf_forte_2006, editor = {Elie Najm and Jean-Fran\c{c}ois Pradat-Peyre and V{\'e}ronique Donzeau-Gouge},
  title = {Formal Techniques for Networked and Distributed Systems - FORTE 2006, 26th IFIP WG 6.1 International Conference, Paris, France, September 26-29, 2006},
  booktitle = {FORTE},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4229},
  year = {2006},
  isbn = {3-540-46219-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,inproceedings] bibtex
  L. Lamport, "The +CAL Algorithm Language," in FORTE, 2006, p. 23.
  @inproceedings{DBLP_conf_forte_Lamport06,
  author = {Leslie Lamport},
  title = {The +CAL Algorithm Language},
  booktitle = {FORTE},
  year = {2006},
  pages = {23},
  ee = {http://dx.doi.org/10.1007/11888116_2},
  crossref = {DBLP:conf/forte/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,inproceedings] bibtex
  L. Lamport, "Checking a Multithreaded Algorithm with +CAL," in DISC, 2006, pp. 151-163.
  @inproceedings{DBLP_conf_wdag_Lamport06,
  author = {Leslie Lamport},
  title = {Checking a Multithreaded Algorithm with +CAL},
  booktitle = {DISC},
  year = {2006},
  pages = {151-163},
  ee = {http://dx.doi.org/10.1007/11864219_11},
  crossref = {DBLP:conf/wdag/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,proceedings] bibtex
  Distributed Computing, 20th International Symposium, DISC 2006, Stockholm, Sweden, September 18-20, 2006, ProceedingsSpringer, 2006.
  @proceedings{DBLP_conf_wdag_2006, editor = {Shlomi Dolev},
  title = {Distributed Computing, 20th International Symposium, DISC 2006, Stockholm, Sweden, September 18-20, 2006, Proceedings},
  booktitle = {DISC},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4167},
  year = {2006},
  isbn = {3-540-44624-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,proceedings] bibtex
  Fifth IEEE International Symposium on Network Computing and Applications, NCA 2006, 24-26 July 2006, Cambridge, Massachusetts, USAIEEE Computer Society, 2006.
  @proceedings{DBLP_conf_nca_2006, title = {Fifth IEEE International Symposium on Network Computing and Applications, NCA 2006, 24-26 July 2006, Cambridge, Massachusetts, USA},
  booktitle = {NCA},
  publisher = {IEEE Computer Society},
  year = {2006},
  isbn = {0-7695-2640-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2006,inproceedings] bibtex
  L. Lamport, "The +CAL Algorithm Language," in NCA, 2006, p. 5.
  @inproceedings{DBLP_conf_nca_Lamport06,
  author = {Leslie Lamport},
  title = {The +CAL Algorithm Language},
  booktitle = {NCA},
  year = {2006},
  pages = {5},
  ee = {http://doi.ieeecomputersociety.org/10.1109/NCA.2006.52},
  crossref = {DBLP:conf/nca/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2005,inproceedings] bibtex
  L. Lamport, "Real-Time Model Checking Is Really Simple," in CHARME, 2005, pp. 162-175.
  @inproceedings{DBLP_conf_charme_Lamport05,
  author = {Leslie Lamport},
  title = {Real-Time Model Checking Is Really Simple},
  booktitle = {CHARME},
  year = {2005},
  pages = {162-175},
  ee = {http://dx.doi.org/10.1007/11560548_14},
  crossref = {DBLP:conf/charme/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2005,inproceedings] bibtex
  B. G. F. V. S. Zambrovski, "Enabling the usage of formal methods by creation of convenient tools," in 2nd International Workshop on Web Services and Formal Methods, Versailles, France, 2005.
  @inproceedings{GVZ2005,
  author = {Boris Gruschko; Friedrich Vogt; Simon Zambrovski},
  title = {Enabling the usage of formal methods by creation of convenient tools},
  booktitle = {2nd International Workshop on Web Services and Formal Methods},
  address = {Versailles, France},
  day = {1-3},
  month = Sep, year = {2005},
  url = {http://www.ti5.tu-harburg.de/publication/2005/Paper/WSFM05-TLATools.pdf},
  abstract = {Creation of formal specifications is being considered a relief for the difficulties of inception and construction of distributed systems. Numerous formal methods exist for the purpose of description of distributed systems and protocols. The creation of formal specifications for these systems lacks the extensive support by tools vendors. This results in lack of sophisticated tools, which help the developer to overcome the initial training investment, shallowing the learning curve. Thus, the development of formal specification for the systems under construction stays an expensive undertaking, which lacks the immediate results, important for the overall acceptance of formal methods by the industry. In this paper we describe a plugin for the Eclipse IDE, developed to simplify the task of authoring formal specifications in the TLA+ environment. This plugin provides features, expected from an IDE for a common programming language, such as syntax highlighting, autocompletion and execution assistance.}
}
• [2005,proceedings] bibtex
  Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, ProceedingsSpringer, 2005.
  @proceedings{DBLP_conf_charme_2005, editor = {Dominique Borrione and Wolfgang J. Paul},
  title = {Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbr{\"u}cken, Germany, October 3-6, 2005, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3725},
  year = {2005},
  isbn = {3-540-29105-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2004,article] bibtex
  J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, "Formal Specification of a Web Services Protocol," Electr. Notes Theor. Comput. Sci., vol. 105, pp. 147-158, 2004.
  @article{DBLP_journals_entcs_JohnsonLLV04,
  author = {James E. Johnson and David E. Langworthy and Leslie Lamport and Friedrich H. Vogt},
  title = {Formal Specification of a Web Services Protocol},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {105},
  year = {2004},
  pages = {147-158},
  ee = {http://dx.doi.org/10.1016/j.entcs.2004.02.022},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2003,article] bibtex
  R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. R. Tuttle, and Y. Yu, "Checking Cache-Coherence Protocols with TLA+," Formal Methods in System Design, vol. 22, iss. 2, pp. 125-131, 2003.
  @article{DBLP_journals_fmsd_JoshiLMTTY03,
  author = {Rajeev Joshi and Leslie Lamport and John Matthews and Serdar Tasiran and Mark R. Tuttle and Yuan Yu},
  title = {Checking Cache-Coherence Protocols with TLA+},
  journal = {Formal Methods in System Design},
  volume = {22},
  number = {2},
  year = {2003},
  pages = {125-131},
  ee = {http://dx.doi.org/10.1023/A:1022969405325},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2002,inproceedings] bibtex
  L. Lamport, J. Matthews, M. R. Tuttle, and Y. Yu, "Specifying and verifying systems with TLA+," in ACM SIGOPS European Workshop, 2002, pp. 45-48.
  @inproceedings{DBLP_conf_sigopsE_LamportMTY02,
  author = {Leslie Lamport and John Matthews and Mark R. Tuttle and Yuan Yu},
  title = {Specifying and verifying systems with TLA+},
  booktitle = {ACM SIGOPS European Workshop},
  year = {2002},
  pages = {45-48},
  ee = {http://doi.acm.org/10.1145/1133373.1133382},
  crossref = {DBLP:conf/sigopsE/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [2002,proceedings] bibtex
  Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002ACM, 2002.
  @proceedings{DBLP_conf_sigopsE_2002, editor = {Gilles Muller and Eric Jul},
  title = {Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002},
  booktitle = {ACM SIGOPS European Workshop},
  publisher = {ACM},
  year = {2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,inproceedings] bibtex
  H. Akhiani, D. Doligez, P. Harter, L. Lamport, J. Scheid, M. R. Tuttle, and Y. Yu, "Cache Coherence Verification with TLA+," in World Congress on Formal Methods, 1999, pp. 1871-1872.
  @inproceedings{DBLP:conf_fm_AkhianiDHLSTY99,
  author = {Homayoon Akhiani and Damien Doligez and Paul Harter and Leslie Lamport and Joshua Scheid and Mark R. Tuttle and Yuan Yu},
  title = {Cache Coherence Verification with TLA+},
  booktitle = {World Congress on Formal Methods},
  year = {1999},
  pages = {1871-1872},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1709/17091871.htm},
  crossref = {DBLP:conf/fm/1999-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,article] bibtex
  P. B. Ladkin, L. Lamport, B. Olivier, and D. Roegel, "Lazy Caching in TLA," Distributed Computing, vol. 12, iss. 2-3, pp. 151-174, 1999.
  @article{DBLP_journals_dc_LadkinLOR99,
  author = {Peter B. Ladkin and Leslie Lamport and Bryan Olivier and Denis Roegel},
  title = {Lazy Caching in TLA},
  journal = {Distributed Computing},
  volume = {12},
  number = {2-3},
  year = {1999},
  pages = {151-174},
  ee = {http://link.springer.de/link/service/journals/00446/bibs/9012002/90120151.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,proceedings] bibtex
  FM’99 – Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume IISpringer, 1999.
  @proceedings{DBLP_conf_fm_1999-2, editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
  title = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II},
  booktitle = {World Congress on Formal Methods},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {1709},
  year = {1999},
  isbn = {3-540-66588-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,proceedings] bibtex
  FM’99 – Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume IISpringer, 1999.
  @proceedings{DBLP_conf_fm_1999-2, editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
  title = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II},
  booktitle = {World Congress on Formal Methods},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {1709},
  year = {1999},
  isbn = {3-540-66588-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,proceedings] bibtex
  Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME ‘99, Bad Herrenalb, Germany, September 27-29, 1999, ProceedingsSpringer, 1999.
  @proceedings{DBLP_conf_charme_1999, editor = {Laurence Pierre and Thomas Kropf},
  title = {Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {1703},
  year = {1999},
  isbn = {3-540-66559-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,inproceedings] bibtex
  Y. Yu, P. Manolios, and L. Lamport, "Model Checking TLA+ Specifications," in CHARME, 1999, pp. 54-66.
  @inproceedings{DBLP_conf_charme_YuML99,
  author = {Yuan Yu and Panagiotis Manolios and Leslie Lamport},
  title = {Model Checking TLA+ Specifications},
  booktitle = {CHARME},
  year = {1999},
  pages = {54-66},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1703/17030054.htm},
  crossref = {DBLP:conf/charme/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1999,inproceedings] bibtex
  H. Akhiani, D. Doligez, P. Harter, L. Lamport, J. Scheid, M. R. Tuttle, and Y. Yu, "Cache Coherence Verification with TLA+," in World Congress on Formal Methods, 1999, pp. 1871-1872.
  @inproceedings{DBLP_conf_fm_AkhianiDHLSTY99,
  author = {Homayoon Akhiani and Damien Doligez and Paul Harter and Leslie Lamport and Joshua Scheid and Mark R. Tuttle and Yuan Yu},
  title = {Cache Coherence Verification with TLA+},
  booktitle = {World Congress on Formal Methods},
  year = {1999},
  pages = {1871-1872},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1709/17091871.htm},
  crossref = {DBLP:conf/fm/1999-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1998,proceedings] bibtex
  CONCUR ‘98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, ProceedingsSpringer, 1998.
  @proceedings{DBLP_conf_concur_1998, editor = {Davide Sangiorgi and Robert de Simone},
  title = {CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {1466},
  year = {1998},
  isbn = {3-540-64896-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1998,inproceedings] bibtex
  E. Cohen and L. Lamport, "Reduction in TLA," in CONCUR, 1998, pp. 317-331.
  @inproceedings{DBLP_conf_concur_CohenL98,
  author = {Ernie Cohen and Leslie Lamport},
  title = {Reduction in TLA},
  booktitle = {CONCUR},
  year = {1998},
  pages = {317-331},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1466/14660317.htm},
  crossref = {DBLP:conf/concur/1998},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
• [1995,article] bibtex
  L. Lamport, "TLA in Pictures," IEEE Trans. Software Eng., vol. 21, iss. 9, pp. 768-775, 1995.
  @article{DBLP_journals_tse_Lamport95,
  author = {Leslie Lamport},
  title = {TLA in Pictures},
  journal = {IEEE Trans. Software Eng.},
  volume = {21},
  number = {9},
  year = {1995},
  pages = {768-775},
  ee = {http://www.computer.org/tse/ts1995/e0768abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}