Sémantika programů

Semestr: zimní 2023/24
Přednáška: Čtvrtek, 14:00, S7 (sudé týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet

Aktuality

1. 1. 2023: Zadání první domácí úlohy je na konci prezentace třetí přednášky. Termín pro odevzdání je 23. 11. 2023.

Přednášky

Datum	Název	Soubory
12. 10. 2023	Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů	Přednáška 1
26. 10. 2023	Indukce	Přednáška 2
9. 11. 2023	Pi a PiVC	Přednáška 3
23. 11. 2023	Částečná správnost	Přednáška 4
7. 12. 2023	Úplná správnost
21. 12. 2023	Strategie pro psaní anotací
11. 1. 2024	Reálné systémy pro verifikaci pomocí kontraktů

Anotace

Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástrojem pro verifikaci vlastností programů. Zápočet bude udělen za vypracování tří domácích úloh menšího rozsahu.

Sylabus

Představení pojmu sémantiky programů
Metody specifikace vlastností imperativních programů
Matematické základy specifikace
Dokazování vlastností programů

Literatura

A. R. Bradley, Z. Manna: The Calculus of Computation, Springer-Verlag, 2007
E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 1999
J. Galenson: PiVC – Verifikující překladač jazyka Pi – https://github.com/jgalenson/piVC (upravený klient pro PiVC systém stáhněte zde).