Stacks Image 10307

Formalna Weryfikacja

Stacks Image 10303
Verification of programs is the Holy Grail of Computer Science.
Andreas Podelski (University of Freiburg)

Opis kursu

Moduł wprowadzający w teoretyczne podstawy weryfikacji programów. Na wykładzie omawiane są takie zagadnienia jak formalna specyfikacja semantyki programów oraz formalne dowodzenie poprawności programów.

Zasady zaliczenia

  • Ocena wystawiana z modułu jest średnią ważoną ocen osiągniętych przez studenta z wykładu (waga 60%) i z laboratorium (waga 40%), przy czym obie oceny muszą być pozytywne.
  • Wiedza oraz kompetencje społeczne sprawdzane są podczas kolokwium jakie odbywa się w ostatnim tygodniu zajęć (ocena z wykładu).
  • Umiejętności studenta sprawdzane są podczas laboratoriów zaliczając listy zadań (ocena z laboratorium).
  • W ostatnim tygodniu zajęć prowadzący laboratoria wysyłają do wykładowcy oceny jakie osiągnęli studenci w ich grupach (nie można zaliczać laboratorium w czasie sesji - ocena z laboratorium musi być wystawiona w ostatnim tygodniu zajęć).
  • Wykładowca oblicza średnią ważoną z ocen z wykładu i z laboratorium a następnie wyliczoną średnią wpisuje studentowi do protokołu w JSOS.

Plan wykładu

Materiały do wykładu powstały na podstawie książki K.R. Apt, F.S. de Boer and E.R. Olderog. Verification of Sequential and Concurrent Programs.

  • Semantyka denotacyjna (2g)
  • Semantyka operacyjna (4g)
  • Programy deterministyczne: programy while (4g)
  • Programy deterministyczne: programy rekurencyjne (2g)
  • Programy deterministyczne: programy rekurencyjne z parametrami (2g)
  • Programy deterministyczne: programy obiektowe (2g)
  • Programy równoległe: rozłączne programy równoległe (2g)
  • Programy równoległe: programy równoległe ze współdzielonymi zmiennymi (4g)
  • Programy równoległe: programy równoległe z synchronizacją (2g)
  • Programy niedeterministyczne (2g)
  • Programy rozproszone (2g)
  • Kolokwium (2g)

Ćwiczenia

Zadania zaczerpnięto z książki K.R. Apt, F.S. de Boer and E.R. Olderog. Verification of Sequential and Concurrent Programs.

  • Lista 0: Wstęp (pierwsze zajęcia)
  • Lista 1: Systemy dowodzenia (drugie zajęcia)
  • Lista 2: Semantyka (trzecie zajęcia)
  • Lista 3: Programy while (czwarte zajęcia)
  • Lista 4: Programy rekurencyjne z parametrami (piąte zajęcia)
  • Lista 5: Programy obiektowe (szóste zajęcia)
  • Lista 6: Programy równoległe ze współdzielonymi zmiennymi (siódme zajęcia)
  • Lista 7: Programy niedeterministyczne (ósme zajęcia)

Laboratoria

Podczas zajęć będziemy używać następujących programów:

  • Lista 0: Wstęp (pierwsze zajęcia)
  • Lista 1: CVC4 i język SMT-LIB (drugie zajęcia)
  • Lista 2: Z3 (trzecie zajęcia)
  • Lista 3: Why3 i język WhyML (szóste zajęcia)
  • Lista 4: Spin i język PROMELA (ósme zajęcia)

Przykłady programów

Literatura

  1. K.R. Apt, F.S. de Boer and E.R. Olderog. Verification of Sequential and Concurrent Programs, Third Edition. Texts in Computer Science, Springer (2009).
  2. G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003).
  3. G. Winskel. The Formal Semantics of Programming Languages. An Introduction. The MIT Press (1994).