References

  1. Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport & Stephan Merz (2008): A TLA+ Proof System. arXiv:0811.1914 [cs]. Available at http://arxiv.org/abs/0811.1914.
  2. Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts & Hernán Vanzetto (2012): TLA+ Proofs. arXiv:1208.5933 [cs], doi:10/dgpd. Available at http://arxiv.org/abs/1208.5933.
  3. Igor Konnov, Jure Kukovec & Thanh-Hai Tran (2019): TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages 3(OOPSLA), pp. 1–30, doi:10.1145/3360549. Available at http://dl.acm.org/citation.cfm?doid=3366395.3360549.
  4. Markus Alexander Kuppe (2014): Distributed TLC. Available at http://tla2014.loria.fr/slides/kuppe.pdf. (Accessed 2016-09-06).
  5. Markus Alexander Kuppe (2019): Visualizing TLA+ Toolbox Error Traces with ShiViz. Available at https://github.com/tlaplus/tlaplus/issues/267#issuecomment-481951259.
  6. Leslie Lamport (1994): The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), pp. 872–923, doi:10.1145/177492.177726. Available at http://portal.acm.org/citation.cfm?doid=177492.177726.
  7. Leslie Lamport (1995): How to Write a Proof. The American mathematical monthly 102(7), pp. 600–608, doi:10.2307/2974556. Available at http://www.jstor.org/stable/2974556.
  8. Leslie Lamport (2003): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston.
  9. Leslie Lamport (2009): The PlusCal Algorithm Language. In: Martin Leucker & Carroll Morgan: Theoretical Aspects of Computing - ICTAC 2009 5684. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 36–60, doi:10/dcd6gv. Available at http://link.springer.com/10.1007/978-3-642-03466-4_2.
  10. Leslie Lamport (2012): How to Write a 21st Century Proof. Journal of Fixed Point Theory and Applications 11(1), pp. 43–63, doi:10.1007/s11784-012-0071-6. Available at http://link.springer.com/10.1007/s11784-012-0071-6.
  11. Leslie Lamport (2018): Using TLC to Check Inductive Invariance. Available at http://lamport.azurewebsites.net/tla/inductive-invariant.pdf. (Accessed 2018-08-16).
  12. Leslie Lamport (2019): Proving Safety Properties. Available at https://lamport.azurewebsites.net/tla/proving-safety.pdf.
  13. Leslie Lamport & Lawrence C. Paulson (1999): Should Your Specification Language Be Typed. ACM Transactions on Programming Languages and Systems 21(3), pp. 502–526, doi:10.1145/319301.319317. Available at http://portal.acm.org/citation.cfm?doid=319301.319317.
  14. D. Marples & P. Kriens (Dec./2001): The Open Services Gateway Initiative: An Introductory Overview. IEEE Communications Magazine 39(12), pp. 110–114, doi:10.1109/35.968820. Available at http://ieeexplore.ieee.org/document/968820/.
  15. Jeff McAffer, Jean-Michel Lemieux & Chris Aniszczyk (2010): Eclipse Rich Client Platform, 2nd ed edition, The Eclipse Series. Addison-Wesley, Upper Saddle River, NJ. OCLC: ocn262433527.
  16. Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker & Michael Deardeuff (2015): How Amazon Web Services Uses Formal Methods. Communications of the ACM 58(4), pp. 66–73, doi:10.1145/2699417. Available at http://dl.acm.org/citation.cfm?doid=2749359.2699417.
  17. J. Steven Perry (2002): Java Management Extensions, 1st ed edition. O'Reilly, Beijing ; Cambridge [Mass.].
  18. Amir Pnueli (1977): The Temporal Logic of Programs. IEEE, pp. 46–57, doi:10.1109/SFCS.1977.32. Available at http://ieeexplore.ieee.org/lpdocs/epic03/wrapper.htm?arnumber=4567924.
  19. William Schultz (2018): An Animation Module for TLA+. Available at https://easychair.org/smart-slide/slide/8V76#.
  20. P. Shannon (2003): Cytoscape: A Software Environment for Integrated Models of Biomolecular Interaction Networks. Genome Research 13(11), pp. 2498–2504, doi:10.1101/gr.1239303. Available at http://www.genome.org/cgi/doi/10.1101/gr.1239303.
  21. Yuan Yu, Panagiotis Manolios & Leslie Lamport (1999): Model Checking TLA+ Specifications. In: Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Laurence Pierre & Thomas Kropf: Correct Hardware Design and Verification Methods 1703. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 54–66, doi:10/fr3fsd. Available at http://link.springer.com/10.1007/3-540-48153-2_6.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org