TLA+ for programmers

This page contains links to the slides and code from my talk “TLA+ for programmers: Building confidence in concurrent code using a model checker”.

Here’s the blurb for the talk:

As developers, we have a number of well-known practices to ensure code quality, such as unit tests, code review and so on. But these practices often break down when we need to design concurrent systems. Often, there can be subtle and serious bugs that are not found with conventional practices.

But there’s another approach that you can use – model-checking – that can detect potential concurrency errors at design time, and so dramatically increase your confidence in your code. In this talk, I’ll demonstrate and demystify TLA+, a powerful design and model-checking system. We’ll see how it can check your concurrent designs for errors, saving you time up front and frustration later!

Slides from NDC Oslo, Jun 10, 2020

Here are some more links to TLA+ related material.

• TLA+ Home Page. The definitive starting point on Leslie Lamport’s site, with a video course, the TLA book, short papers, etc.
• LearnTLA.com, a website and book by Hillel Wayne (who also does trainings)

There are lots and lots of other good ones as well – just search the net for “TLAplus”