A meeting of the TLA+ community will be organized along ABZ 2014 on June 3, 2014, in Toulouse, France.It will consist of two tutorials, focusing on recent additions to the TLA+ tools, contributed presentations by members of the TLA+ community, and discussions on further development of the language and tool support.Contributed talks should present work of interest to users of TLA+ or PlusCal, such as:
- industrial and academic case studies,
- new tools for TLA+,
- innovative use of existing tools or reports on their shortcomings,
- use of TLA+ in education.
The presentations should be informal and leave sufficient time for discussions. There will not be formal proceedings, and presentations of relevant work published elsewhere are welcome. Proposals for presentations, with a short (1-2 page) abstract summarizing the content, should be sent by April 25, 2014 to tla...@xxxxxxxx. Notification will be given by April 29, 2014. The abstracts and presentations given at the event will be made available on the Web. Full information about the event is available at tla2014.loria.fr.Participants are required to register using the ABZ registration form. The deadline for the early registration fee is on April 30, 2014.The tutorials will be:Markus Alexander Kuppe: Distributed TLCTLC is an explicit-state model checker for verifying safety and liveness properties of finite instances of TLA+ specifications. The tutorial will give a brief overview on TLC in general and then focus on recent extensions that support running TLC on a cluster of distributed computing nodes.Tomer Libal and Stephan Merz: The TLA+ Proof SystemTLAPS is an interactive proof environment for TLA+. Recent developments have focused on library modules, and on the addition of elementary temporal reasoning. The tutorial will present the current state of TLAPS and illustrate its use for verifying properties of TLA+ specifications.––––––––Also note that Leslie Lamport will be an invited speaker at the ABZ conference.