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áška 3. ledna 2018 je zrušena. V případě zájmu o konzultaci mě prosím kontaktujte e-mailem.
  • 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<at-sign>d3s.mff.cuni.cz nebo pomocí příkazu submit programu PiVC. Termín pro odevzdání řešení třetí úlohy je 26. ledna 2018, 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<at-sign>d3s.mff.cuni.cz nebo pomocí příkazu submit programu PiVC. Termín pro odevzdání řešení druhé úlohy je 13. prosince 2017, 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<at-sign>d3s.mff.cuni.cz nebo pomocí příkazu submit programu PiVC. Termín pro odevzdání řešení první úlohy je 15. listopadu 2017, 23:59.

Přednášky

DatumNázev přednáškySoubory
04.10.2017 Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů prednaska01.pdf
18.10.2017 Indukce prednaska02.pdf | LinearSearch.pi
01.11.2017 Pi a PiVC prednaska03.pdf
15.11.2017 Použití Pi pro ověření částečné správnosti prednaska04.pdf | InsertionSort.pi | UnsortedUnion.pi
29.11.2017 Ověření úplné správnosti (terminace) prednaska05.pdf | BubbleSort.pi | QuickSort.pi | MergeSort.pi | Zetony.pi
13.12.2017 Strategie pro psaní anotací prednaska06.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-04-12