Sémantika programů – NSWI162

Model Checking
Výuka: Zimní semestr 2017/2018
Středa 14:00 v S7, 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

Přednášky

DatumNázev přednáškySoubory
04.10.2017 Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů
18.10.2017 Indukce

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 2017-08-16