I’m a fan of the video course too, but having said that it will not actually teach you TLA+. For that you really need to study the book and the sample specs in the toolkit, but after the first 2 short (and delightful) videos you will have an understanding of what TLA+ is and what it (might) be useful for. The next 2 videos give you a deeper look.
Nice list. You should add @hwayne’s learntla.com to that list. It entices beginners by giving them real-world examples in a useful subset of it. Also, Refinement Calculus: A Systematic Introduction looked like a comprehensive treatment of refinement. I found it useful just for the first chapter defining everything in terms of benign or malicious agents interacting with contracts. Very neat read even for a guy like me who can’t follow the logic stuff.
Finally, we need Alloy and rewriting logic (esp Maude) on that list. Alloy because it’s the TLA+ of model-checking program structure. Most report it’s easy to use with intro’s and examples on web page. Rewriting logic makes things like transformations and equivalence checks easier with a big, formal semantics of C (KCC) done w/ K Framework on Maude. One work also caught errors in Eiffel’s SCOOP model for concurrency with it. Powerful stuff that gets less attention than Coq, Isabelle, etc.
Thanks for the link to the tutorial! Although I don’t add any tutorials to the list because it’s a first source of knowledge if you want to learn tool or program and tutorials are always free so everyone can easily find.
…and video courses
I can highly recommend the TLA+ video course, if only for the nice outfits of Leslie.
http://lamport.azurewebsites.net/video/videos.html
I’m a fan of the video course too, but having said that it will not actually teach you TLA+. For that you really need to study the book and the sample specs in the toolkit, but after the first 2 short (and delightful) videos you will have an understanding of what TLA+ is and what it (might) be useful for. The next 2 videos give you a deeper look.
What book could you recommend about TLA+?
Lamport’s book, https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/ , Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers , also available as a free PDF.
One major limitation of Specifying Systems is that it was written in 2004, so it misses some of the more modern features of TLA+, like PlusCal, recursive operators and lambdas, and TLC debugging tools.
Nice list. You should add @hwayne’s learntla.com to that list. It entices beginners by giving them real-world examples in a useful subset of it. Also, Refinement Calculus: A Systematic Introduction looked like a comprehensive treatment of refinement. I found it useful just for the first chapter defining everything in terms of benign or malicious agents interacting with contracts. Very neat read even for a guy like me who can’t follow the logic stuff.
http://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf
Finally, we need Alloy and rewriting logic (esp Maude) on that list. Alloy because it’s the TLA+ of model-checking program structure. Most report it’s easy to use with intro’s and examples on web page. Rewriting logic makes things like transformations and equivalence checks easier with a big, formal semantics of C (KCC) done w/ K Framework on Maude. One work also caught errors in Eiffel’s SCOOP model for concurrency with it. Powerful stuff that gets less attention than Coq, Isabelle, etc.
http://alloy.mit.edu/alloy/
http://maude.cs.illinois.edu/w/index.php?title=The_Maude_System
Each of these have a book but the web sites themselves are more valuable for overall information they have.
I feel the Isabelle/HOL tutorial is worth mentioning in this list: https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1/doc/tutorial.pdf
Thanks for the link to the tutorial! Although I don’t add any tutorials to the list because it’s a first source of knowledge if you want to learn tool or program and tutorials are always free so everyone can easily find.