Paweł Szulc — Formal specification applied (with TLA+) (45 minutes)


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

 

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *