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 No
Egzamin Yes
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)