Semestr: zimní 2022/23
Přednáška: Úterý, 10:40, SU2 (liché týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Přednáška: Úterý, 10:40, SU2 (liché týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Aktuality
- 20.12.2002: Zadání třetí domácí úlohy je v prednaska06.pdf. Termín pro odevzdání je 13. 1. 2023.
- 5.12.2022: Zadání druhé domácí úlohy je v prednaska05.pdf. Termín pro odevzdání je 20. 12. 2022.
- 8.11.2022: Zadání první domácí úlohy je v prednaska03.pdf. Termín pro odevzdání je 22. 11. 2022.
Přednášky
| Datum | Název | Soubory |
|---|---|---|
| 11. 10. 2022 | Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů | Přednáška 1 |
| 25. 10. 2022 | Indukce | Přednáška 2 |
| 08. 11. 2022 | Pi a PiVC | Přednáška 3, Příklady |
| 22. 11. 2022 | Částečná správnost | Přednáška 4, Příklady |
| 6. 12. 2022 | Úplná správnost | Přednáška 5, Příklady |
| 20. 12. 2022 | Strategie pro psaní anotací, reálné systémy pro verifikaci pomocí kontraktů | Přednáška 6, Příklady |
| 20. 12. 2022 | Reálné systémy pro verifikaci pomocí kontraktů | Přednáška 7 |
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).