W ciągu ostatnich 30 lat rozwoju informatyki pojawiło się wiele narzędzi
umożliwiających formalizację i mechaniczną (a dla pewnych klas problemów
automatyczną) weryfikację twierdzeń dotyczących zarówno teorii matematycznych,
jak i np. programów komputerowych. Jednym z powszechnie używanych obecnie
systemów wspomagających dowodzenie twierdzeń 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 wykładu jest wyposażenie studentów w umiejętność praktycznego
wykorzystania narzędzi wspierających dowodzenie - takich jak Coq - do
modelowania i weryfikacji zagadnień z różnych obszarów informatyki.
Plan:
1\. Podstawy systemu Coq i interaktywnego dowodzenia twierdzeń.
2\. Omówienie wybranych formalizacji (np. certyfikowany kompilator C, dowód
twierdzenia o 4 kolorach, protokoły kryptograficzne) - przewidywane są
prezentacje wybranych zagadnień przez studentów.
3\. Projekty studenckie.
Wymagania **:** Logika dla informatyków, przyda się znajomość jakiegoś języka
funkcyjnego
