Sémantika programů – NSWI162

Model Checking
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<at-sign>d3s.mff.cuni.cz
Informace v SIS: NSWI162

Aktuality

  • 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

DatumNázev přednáškySoubory
05.10.2018 Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů prednaska01.pdf
19.10.2018 Indukce prednaska02.pdf | LinearSearch.pi
02.11.2018 Pi a PiVC prednaska03.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).
Modified on 2018-11-02