Formal specification applied (with TLA+)

Elevator pitch

Formal verification promises software without bugs. At the same time, even its name scares programmers away ("It's math! run for your lives!"). This talk will familiarize you with one form of formal verification: a model checker - one that is available in a formal specification tool called TLA+.

Description

Formal methods (and formal verification) promise something that every programmer dream about - an ability to deliver software that is proven not to fail. Despite them being heavily researched for the past few decades, they seem not to get enough traction. It might be that people are just simply scared of a little bit of math or it could be that even good techniques take time to surface to the mainstream. This talk is here to change that. To convince and encourage you that (at least) some techniques are easy to use and can potentially save you days or even weeks of later debugging.
Pawel 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 will use in your daily routines. Working with TLA+ will also allow you to think more abstractly about your system. This is not a theoretical talk, this lecture begs you to "please try it at home" you won't be disappointed.

Language: English

Presented by: Paweł Szulc
Pawel 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.