Seminarium będzie poświęcone metodom weryfikacji programów opartym na logice
separacyjnej. W pierwszej części zajmiemy się teorią (wnioskowanie o
programach w językach z mutowalnym stanem, współbieżnych, obiektowych). W
drugiej części zapoznamy się z narzędziami wspierającymi automatyzację
wnioskowania z wykorzystaniem logiki separacyjnej (m. in. jStar, Facebook
Infer). **
**
**Wymagania:** Logika dla informatyków, Metody programowania, Teoretyczne
podstawy języków programowania
