International Workshop on the TLA+ Method and Tools
27 August 2012
Paris, France (satellite of FM 2012)
08:00-09:00 |
Registration and continental breakfast |
|
09:00-10:30 |
Session 1: TLA+ Tools |
|
| 09:00 | Dominik Hansen, Michael Leuschel: TLA2B – A New Validation Tool for TLA+ |  |
| 09:30 | Markus A. Kuppe: Current State of Distributed TLC | |
| 10:00 | Stephan Merz, Hernán Vanzetto: Harnessing SMT Solvers for TLA+ Proofs | |
10:30-11:00 |
Coffee Break |
|
11:00-12:30 |
Session 2: Experience Using TLA+ |
|
| 11:00 | Chris Newcombe: Experience of Software Engineers Using TLA+, PlusCal and TLC | |
| 11:30 | Tianxiang Lu, Stephan Merz, Christoph Weidenbach: Formal Verification of Pastry Using TLA+ | |
| 12:00 | Thomas L. Rodeheffer, Ramakrishna Kotla: Inserting Intentional Bugs for Model Checking Assurance |  |
12:30-14:00 |
Lunch |
|
14:00-15:30 |
Session 3: Theory and Teaching |
|
| 14:00 | Paul-David Brodmann, Hannes Lau, Uwe Nestmann: Automated Generation of Refinement Mappings | |
| 14:30 | Philippe Mauran, Philippe Quéinnec, Xavier Thirioux: Teaching Transition Systems and Formal Specifications with TLA+ | |
| 15:00 | Paul Tavolato, Friedrich Vogt: Integrating Formal Methods into Computer Science Curricula at a University of Applied Sciences |
|
15:30-16:00 |
Coffee Break |
|
16:00-17:00 |
Discussion: Current and Future State of TLA+ |
|
