"Specifying distributed systems with TLA+" workshop with Paweł Szulc

Event Information

Share this event

Date and Time

Location

Location

ILEC Conference Centre

47 Lillie Road

London

SW6 1UD

United Kingdom

View Map

Refund Policy

Refund Policy

Refunds up to 30 days before event

Eventbrite's fee is nonrefundable.

Event description

Description

Paweł Szulc is a well known developer in the community, and his presentations and workshop about TLA+ have been widely acclaimed as 'must see' for all interested in the subject.

In this training Paweł will introduce Leslie Lamport's TLA+ - a formal specification tool with a model checker and proof system. The main objective is to see how formal specification can quickly discover issues deeply hidden in the corner cases of your design. You will gain a powerful tool that you can use in your day job. Working with TLA+ will also allow you to think more abstractly about your system. By using TLA+ you will make sure your software is more resilient and has fewer bugs.

Elevator Pitch

Learn how to use TLA+ to study, design and specify your algorithms. This workshop is designed to teach you about TLA+ from the ground up. We will start with simple distributed algorithms and slowly move toward more complex ones. Knowledge you gain can be immediately applied at work the day after the workshop.

Details

TLA+ is a formal specification language developed by Leslie Lamport, designed to specify, model, document, and verify concurrent systems. It empowers your ability to clearly specify your design choices by using a formal specification, but even more importantly it can also formally verify that your design choice is correct — meaning that it is both safe (does not break any rules) and live (over time it converges toward the result).

This workshop is designed to teach you about TLA+ from the ground up. We will start with simple distributed algorithms and slowly move toward more complex ones. In each section, a bit of TLA+ notation will be introduced, followed by the description of the algorithm that we will specify. Lastly, we will run the model checker to look for potential errors in our design. Each section will end with an exercise. This will be an intensive six hours, but at the end of the day it will be hard not to notice that your core engineering skills got a lot better.

We will use well known distributed algorithms as examples (such as Two Phase Commit or Paxos), but the knowledge you gain can be applied to your own systems. The objective of this workshop is to equip attendees with powerful tools that will allow them to better design their systems and have stronger guarantees that they will be correct. Lastly, working with TLA+ will also allow you to think more abstractly about your system, and that has a value on its own.

This is a 1 day workshop for a medium sized group. You will need to bring your own laptop.

Location: ILEC Conference Centre, Earl's Court, London

Language: English

Intended audience: No formal verification experience necessary

Refreshments: The ticket price includes lunch and tea/coffee breaks

Presented by: Paweł Szulc

Paweł Szulc is primarily a programmer. Always was and always will be. Experienced professionally in JVM ecosystem, currently having tons of fun with Scala and Haskell. Humble apprentice of Functional Programming. Runs a blog rabbitonweb.com.

Share with friends

Date and Time

Location

ILEC Conference Centre

47 Lillie Road

London

SW6 1UD

United Kingdom

View Map

Refund Policy

Refunds up to 30 days before event

Eventbrite's fee is nonrefundable.

Save This Event

Event Saved