Semestr: zimní 2020/21
Přednáška: Pátek, 10:40, SU1 (liché týdny – sudé kalendářní) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Přednáška: Pátek, 10:40, SU1 (liché týdny – sudé kalendářní) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
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).