[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] teaching TLA



Dear Daniel Leivant,

Leslie's hyperbook is an obvious source for many ideas for such a course, it is essentially a tutorial: http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html.

I have occasionally given TLA courses at summer schools, and I'll send you a set of slides off-list. For a description that focuses more on the logic of TLA, you may find some material in http://www.loria.fr/~merz/papers/tla+logic2008.html.

The TLA+ distribution comes with a set of a few examples for the use of the model checker. I'm not sure if these are part of the TLA+ Toolbox distribution of TLC, but they are (or at least used to be) part of the standalone (command-line) tools available from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html#downloading.

Best regards,

Stephan

On 16 Dec 2013, at 18:04, Daniel Leivant <lei...@xxxxxxxxxxxxxx> wrote:

I plan to incorporate next semester an introduction to TLA (and temporal logic) into a graduate introductory course on formal logic and program verification.
If anyone has any ideas, material, pointers, or experience to share, that would be tremendously helpful and greatly appreciated.

Thanks much in advance and best wishes  - Daniel

Daniel Leivant
Professor of computer science
and adjunct professor of mathematics
Indiana University Bloomington

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.