Formal verification applied (with TLA+)

gistfile1.txt

1 Formal specification applied (with TLA+)
=========================================

1.1 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+.


1.2 Description
~~~~~~~~~~~~~~~

  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 on 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.