Semestr: zimní 2021/22
Přednáška: Čtvrtek, 12:20, SU2 (liché týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Přednáška: Čtvrtek, 12:20, SU2 (liché týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Aktuality
- 05.01.2022: Zadání třetí domácí úlohy je v lecture06.pdf. Termín pro odevzdání je 21. 1. 2022, stejně jako u druhé úlohy.
- 16.12.2021: Zadání druhé domácí úlohy je v lecture05.pdf. Termín pro odevzdání je 21. 1. 2022.
- 15.11.2021: Přednáška, která se měla konat 9.12.2021, se přesouvá na termín 16.12.2021. V původně plánovaném termínu 9.12.2021 proběhne přednáška z předmětu Úvod do middleware.
- 10.11.2021: Zadání první domácí úlohy je v lecture03.pdf. Termín pro odevzdání je 25. 11. 2021.
Přednášky
| Datum | Název | Soubory |
|---|---|---|
| 30. 9. 2021 | Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů | lecture01.pdf |
| 14. 10. 2021 | Indukce | lecture02.pdf, examples02.zip |
| 11. 11. 2021 | Pi a PiVC | lecture03.pdf, examples03.zip |
| 25. 11. 2021 | Částečná správnost | lecture04.pdf, examples04.zip |
| 16. 12. 2021 | Úplná správnost | lecture05.pdf, examples05.zip |
| 6. 1. 2022 | Strategie pro psaní anotací | lecture06.pdf, examples06.zip |
| 6. 1. 2022 | Reálné systémy pro verifikaci pomocí kontraktů | lecture07.pdf |
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 malé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).