1. 34
  1.  

  2. 6

    …and video courses

    1. 6

      I can highly recommend the TLA+ video course, if only for the nice outfits of Leslie.

      http://lamport.azurewebsites.net/video/videos.html

      1. 5

        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.

        1. 1

          What book could you recommend about TLA+?

          1. 3

            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.

            1. 2

              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.

    2. 6

      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.

      1. 3

        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

        1. 1

          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.