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