Sémantika programů (NSWI162)

Výuka: Zimní semestr 2018/2019
Pátek 9:00 v SU2, liché týdny (sudé kalendářní)
Garantováno: Katedra distribuovaných a spolehlivých systémů
Zakončení: Zápočet
Přednášející: Jan Kofroň
e-mail: jan.kofron@d3s.mff.cuni.cz
Informace v SIS: NSWI162
*

Aktuality

  • Zadání třetí domácí úlohy je na posledním snímku šesté přednášky. Řešení úlohy zašlete mailem na nswi162@d3s.mff.cuni.cz. Termín pro odevzdání řešení první úlohy je 25. ledna 2019, 23:59.
  • Zadání druhé domácí úlohy je na posledním snímku páté přednášky. Řešení úlohy zašlete mailem na nswi162@d3s.mff.cuni.cz. Termín pro odevzdání řešení první úlohy je 14. prosince 2018, 23:59.
  • Zadání první domácí úlohy je na posledním snímku třetí přednášky. Řešení úlohy zašlete mailem na nswi162@d3s.mff.cuni.cz. Termín pro odevzdání řešení první úlohy je 16. listopadu 2018, 23:59.

Přednášky

Datum
Název
Soubory
05. 10. 2018
Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů
19. 10. 2018
Indukce
02. 11. 2018
Pi a PiVC
16. 11. 2018
Částečná správnost
14. 12. 2018
Strategie pro psaní anotací
04. 01. 2019
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 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).