Weryfikacja programów w systemie Coq lato 2023/24

Język wykładowy Polski
Opiekun Małgorzata Biernacka
Liczba godzin 30 (wyk.) 30 (prac.)
Rodzaj I2.Z - zastosowania inf.
ECTS 6
Polecany dla I roku No
Egzamin Yes

Opis przedmiotu:

Przedmiot będzie współprowadzony z D. Biernackim. Jednym z powszechnie używanych obecnie systemów wspomagających dowodzenie twierdzeń (nie tylko w środowisku akademickim) jest system Coq (<http://coq.inria.fr/>), oparty na rachunku konstrukcji z definicjami indukcyjnymi. Coq pozwala na definiowanie funkcji i predykatów, wyrażanie twierdzeń matematycznych i specyfikacji oprogramowania, a także na interakcyjne przeprowadzanie formalnych, weryfikowanych przez system dowodów takich twierdzeń oraz generowanie certyfikowanego kodu. Celem przedmiotu jest wyposażenie studentów w umiejętność praktycznego wykorzystania systemu Coq do modelowania i weryfikacji oprogramowania. Przedmiot będzie prowadzony na podstawie materiałów Software Foundations (<https://softwarefoundations.cis.upenn.edu>), w szczególności rozdziałów Logical Foundations, Programming Language Foundations (fragmenty) i Separation Logic Foundations. Wymagania: -- Logika dla informatyków -- przyda się znajomość jakiegoś języka funkcyjnego Zakres tematyczny: 1. Wprowadzenie do Coqa. 2. Logika Hoare'a. 3. Logika separacyjna. 4. Jeśli czas pozwoli, popatrzymy na Iris (https://iris-project.org/)

Wykłady

Lista
Prowadzący Termin zajęć Limit Zapisani Kolejka
Dariusz Biernacki
śr 12:00-14:00 (s. 140) 15 13 0

UWAGA! Wyższa liczba oznacza wyższy priorytet, po zapisaniu do grupy zostajemy usunięci z kolejek o niższym priorytecie.

Pracownie

Lista
Prowadzący Termin zajęć Limit Zapisani Kolejka
Dariusz Biernacki
śr 14:00-16:00 (s. 140) 15 13 0

UWAGA! Wyższa liczba oznacza wyższy priorytet, po zapisaniu do grupy zostajemy usunięci z kolejek o niższym priorytecie.


Konsultacje prowadzących:


Imię i nazwisko Pokój Konsultacje
Dariusz Biernacki 242 wtorek 14-16 (po uzgodnieniu przez e-mail)