Important dates

submission: April 25
notification:   April 29
workshop: June 3

Contact

tla2014@inria.fr

08:45-09:00
Registration
09:00 Stephan Merz: A Tutorial Introduction to TLA+ slides    TLA specs
10:00 Amira Methni, Matthieu Lemerre, Belgacem Ben Hedia, Serge Haddad, Kamel Barkaoui: C2TLA+ – A translator from C to TLA+ slides
10:30-11:00
Coffee Break
11:00 Markus A. Kuppe: Distributed TLC slides    screencast
12:00 Dominik Hansen, Jens Bendisposto, Michael Leuschel: Integrating ProB into the TLA Toolbox slides
12:30-14:00
Lunch
14:00 Jael Kriener, Tomer Libal, Tom Rodeheffer: The TLA+ Proof System slides
15:30-16:00
Coffee Break
16:00 General discussion on TLA+: method, applications, and tools

The program consists of a mix of tutorials on the TLA+ specification language and its supporting tools. The tutorials do not assume previous knowledge of TLA+ or the tools. Participants are strongly encouraged to install the TLA Toolbox and the TLA+ Proof System on their laptops.

Participants must register through the ABZ registration page.

Abstracts of tutorials

Stephan Merz: A Tutorial Introduction to TLA+

TLA+ is a specification language that combines mathematical set theory for describing the static aspects of systems and the Temporal Logic of Actions for modeling the dynamic aspects. It is mainly intended for the specification of distributed and concurrent algorithms. This tutorial will give a hands-on introduction to the language and its tool support.

Markus A. Kuppe: Distributed TLC

TLC 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.

Jael Kriener, Tomer Libal, Tom Rodeheffer: The TLA+ Proof System

TLAPS 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.