У курсі подано баланс теорії та практики моделювання i верифікації програмного забезпечення, зокрема паралельного та розподіленого. Викладені методи являють собою основу для розробки надійного програмного забезпечення. Більшість відомостей про надійність сучасних програм ґрунтується на методах тестування, які гарантують певну вірогідність виконання програмою заданої функції. Формальне доведення коректності програм є наступним кроком підвищення надійності програмного забезпечення для спеціальних застосувань у системах реального часу, а також життєво критичних сферах.