Formal methods (and formal verification) promise something that every programmer dreams 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.