Semestr: zimní 2026/27
Přednáška: Pondělí, 12:20, S1 (Jan Kofroň)
Stránka v SIS: NSWI183
Zakončení: Zápočet
Přednáška: Pondělí, 12:20, S1 (Jan Kofroň)
Stránka v SIS: NSWI183
Zakončení: Zápočet
Stránky z předchozího roku: 2025/26
Aktuality
Přednášky
| Datum | Název | Soubory |
|---|---|---|
| 05. 10. 2026 | Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů | |
| 12. 10. 2026 | Indukce | |
| 19. 10. 2026 | Pi a PiVC | |
| 26. 10. 2026 | Částečná správnost | |
| 02. 11. 2026 | Úplná správnost | |
| 09. 11. 2026 | Strategie pro psaní anotací | |
| 16. 11. 2026 | Reálné systémy pro verifikaci pomocí kontraktů | |
| 23. 11. 2026 | Dafny | |
| 30. 11. 2026 | Dafny | |
| 07. 12. 2026 | Dafny | |
| 14. 12. 2026 | Dafny | |
| 04. 01. 2027 | Dafny |
Anotace
Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástroji pro verifikaci vlastností programů – PiVC a Dafny. Zápočet bude udělen za vypracování tří domácích úloh menšího rozsahu a jedné složitější úlohy.
Sylabus
- Představení pojmu sémantiky programů
- Metody specifikace vlastností imperativních programů
- Matematické základy specifikace
- Dokazování vlastností programů
- Programovací jazyk Dafny
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).
- The Dafny Programming and Verification Language