Teaching
This page contains a list of references and sources for teaching TLA+, PlusCal or just using TLA+ in educational purposes for explanation of various topics of logic or computer science.
- Model Checking, 2009/now, St. Poelten, Austria
- Teaching Formal Methods in a Third World Country: What, Why and How, Rosario National University, Rosario, Argentina
- Verified Software Systems, 2008/2009, TUHH, Germany
- Methods and Models of System Design, 2009, HU, Berlin, Germany
- Networks and Distributed Systems, 2009, Bielefeld University, Bielefeld, Germany
- Software Specification and Verification, 2008/2009, National Taiwan University, Taiwan
If you know a reference not mentioned here, just add a comment to this page.
Model Checking, 2009-now, University of Applied Science, St. Poelten, Austria
Prof. Dr. Friedrich H. Vogt held a research fellow position at SRI International in 1982. At SRI International, where he first met Leslie Lamport he worked with Richard Schwartz and Michael Melliar-Smith on Interval Logic, a higher level temporal logic. From June to October 2003 he was working with Leslie Lamport on specification and model checking of Web Service semantics using TLA+ at MSR SVC. He joined the Connected System Division at Microsoft in Redmond from August to December 2008. Since 2009 he is teaching “Model Checking” (Logic in Computer Science and TLA+) at the UAS St. Poelten, Austria.
Teaching Formal Methods in a Third World Country: What, Why and How, Rosario National University, Rosario, Argentina
We have been teaching formal methods for eight years at two major Argentinean universities. It is hard to find examples of the application of formal methods outside the most advanced industrial sectors. Then, why teach formal methods in a country that hardly produce software for advanced industries? Why formal methods in a country which buy technology instead of creating it? We were one of the first in teaching formal methods in Latin America, likely the first in teaching TLA and CSP… Read the rest of the paper
Networks and Distributed Systems, 2009, Bielefeld University, Bielefeld, Germany
Prof. Dr. Peter Ladkin, the lead of the RVS group at Faculty of Technology at the University of Bielefeld in Germany is using TLA+ in several lectures. Visit the group web page or list of publications.
Methods and Models of System Design, 2009, HU, Berlin, Germany
Prof. Dr. Wolfgang Reisig is teaching “Methods and Models of System Design” at Humbold University of Berlin, Germany. Visit the lecture homepage in German.
Verified Software Systems, 2008/2009, TUHH, Hamburg, Germany
A lecture on Logical Foundations (Propositional logic, predicate logic, Decision problems: Satisfiability, entailment, model checking, model finding), Software abstractions and automated testing of specifications (Alloy) and Temporal Logic of Actions (TLA+, PlusCal) is being taught by Rainer Marrone and Miguel Garcia at STS department of TUHH, Hamburg, Germany.
Visit the Lecture web page and the Lecture slides.
Software Specification and Verification, 2008/2009, National Taiwan University, Taipei, Taiwan
Prof. Yih-Kuen TSAY is teaching several courses related to TLA+ from Fall 2008 to Spring 2009 at Department of Information Management the National University of Taiwan in Taipei. Visit his web page.
