Tagi
systemy sieciowe i komputerowe algorytmika i złożoność obliczeniowa metody numeryczne i grafika komputerowa języki programowania i logika przetwarzanie danych Data Science Praca zespołowa Bazy danych Ekonomia Inżynieria oprogramowania Projektowanie i programowanie obiektowe Architektury systemów komputerowych Systemy operacyjne Sieci komputerowe Ochrona własności intelektualnej Rachunek prawdopodobieństwa i statystykaEfekty kształcenia
Podstawy informatyki i programowania Programowanie i projektowanie obiektowe Architektury systemów komputerowych Rachunek prawdopodobieństwa (L) Systemy operacyjne Sieci komputerowe Bazy danych Podstawy inżynierii oprogramowania Inżynieria oprogramowania (L) Rachunek prawdopodobieństwa (I) Społeczno-ekonomiczne aspekty informatyki (I)Deductive Verification (Q2)
Język wykładowy | Angielski |
---|---|
Semestr | Letni |
Status | W ofercie |
Opiekun | Małgorzata Biernacka |
Liczba godzin | 15 (wyk.) 15 (ćw-prac.) |
Rodzaj | I2.T - teoria inf. |
ECTS | 3 |
Polecany dla I roku | Nie |
Egzamin | Tak |
Tagi | JP (języki programowania i logika) |
Opis przedmiotu:
This is a half-semester course offered in the second half of the spring semester.
The course is an introduction to deductive verification building on the foundational principles of Hoare logic and extending them to modern applications of separation logic (state of the art is Facebook’s Infer verifier). Apart from theoretical exercises, we will spend some time working with Why3 - a tool for deductive program verification.
Topics covered:
-
Hoare logic: foundations, formulation for an ML-like language, application to practical (automated) verification of programs
-
separation logic: motivation and foundations, possible approaches to automatization, other applications (e.g., in concurrency)