Program

Videos of the presentations are available on YouTube.

09:00	David Langworthy. TLA+ in Engineering Systems – Quinceañera (Keynote)
10:00	Valentin Schneider. Modeling Virtual Machines and Interrupts in TLA+ & PlusCal
10:30-11:00	Coffee Break
11:00	William Schultz. An Animation Module for TLA+
11:45	Igor Konnov, Jure Kukovec, Thanh Hai Tran. BMCMT: Bounded Model Checking of TLA+ Specifications with SMT
12:30-14:00	Lunch
14:00	Stefan Resch. Applying TLA+ in a Safety-Critical Railway Project
14:30	Markus Kuppe. State Space Explosion or: How To Fight An Uphill Battle (Tutorial)
15:30-16:00	Coffee Break
16:00	Ioannis Filippidis, Richard M. Murray. Proving properties of a minimal covering algorithm
16:45	Annie Liu, Scott D. Stoller, Saksham Chand, Xuetian Weng. Invariants in Distributed Algorithms
17:30	Discussion and wrap-up
18:00	End of the meeting

Abstracts

David Langworthy. TLA+ in Engineering Systems – Quinceañera

Dave will relate experience and anecdotes from 15 years applying TLA+ in a commercial software engineering environment with a look toward the future.

Valentin Schneider. Modeling Virtual Machines and Interrupts in TLA+ & PlusCal

We present TLA+ and PlusCal specifications of the Arm Generic Interrupt Controller, the KVM hypervisor and their interactions. The objective is to verify safety properties such as correct delivery of interrupts, correct context switching, and correct migration of virtual CPUs, as well as liveness properties such as the eventual delivery of interrupts.

William Schultz. An Animation Module for TLA+

The Animation module is a new TLA+ module which allows for the creation of interactive visualizations of TLC execution traces that can be run inside a web browser. The talk will present an overview of the core concepts of the Animation module and how it works, and then demonstrate a few examples of TLA+ specs that have been animated using the module.

Igor Konnov, Jure Kukovec, Thanh Hai Tran. BMCMT: Bounded Model Checking of TLA+ Specifications with SMT

We present the development version of BMCMT, a symbolic model checker for TLA+. It finds, whether a TLA+ specification satisfies an invariant candidate by checking satisfiability of an SMT formula that encodes: (1) an execution of bounded length, and (2) preservation of the invariant candidate in every state of the execution. Our tool is still in the experimental phase, due to a number of challenges posed by TLA+ semantics to SMT solvers. We will discuss these challenges and our current approach to them in the talk. Our preliminary experiments show that BMCMT scales better than the standard TLA+ model checker TLC for large parameter values, e.g., when a TLA+ specification models a system of 10 processes, though TLC is more efficient for tiny parameters, e.g. when the system has 3 processes.

Stefan Resch. Applying TLA+ in a Safety-Critical Railway Project

The presentation gives an overview on the experience and insights gained from using TLA+ and PlusCal to model and develop fault-tolerant and safety-critical modules for TAS Control Platform, a platform for railway control applications up to safety integrity level 4.

Markus Kuppe. State Space Explosion or: How To Fight An Uphill Battle

In this tutorial we will explore the tricks and techniques available in TLA+, TLC and the TLA Toolbox to squeeze out more performance to check models of interesting sizes despite the state space explosion problem. The tutorial will also shed light on what has been done under the hood so far to scale TLC to modern day hardware and what we are up to next to tackle the state space explosion challenge.

Ioannis Filippidis, Richard M. Murray. Proving properties of a minimal covering algorithm

This work concerns the specification and proof using TLA+ of properties of an algorithm for solving the minimal covering problem, which we have implemented in Python. Minimal covering is the problem of choosing a minimal number of elements from a given set to cover all the elements from another given set, as defined by a given function. The TLA+ modules are available online. The proofs of safety properties in these modules have been checked with the proof assistant TLAPS (version 1.4.3), in the presence of the tools Zenon, CVC4, Isabelle, and LS4. We have been motivated to study and implement this algorithm for converting binary decision diagrams to formulas of small size, so that humans can read the results of symbolic computation.

Annie Liu, Scott D. Stoller, Saksham Chand, Xuetian Weng. Invariants in Distributed Algorithms

We will discuss making invariants explicit in specification of distributed algorithms. Clearly this helps prove properties of distributed algorithms. More importantly, we show that this helps make it easier to express and to understand distributed algorithms at a high level, especially through direct uses of message histories. We will use example specifications in TLA+, for verification of Paxos using TLAPS, as well as complete excutable specifications in DistAlgo, a high-level language for distributed algorithms.