Weryfikacja formalna 1000-2M25WER
1. Model-checking dla skończeniestanowych systemów reaktywnych. Logiki temporalne (LTL, CTL, CTL*), automaty Büchiego.
2. Symbolicze sprawdzanie modeli z użyciem BDD. Redukcje częściowo-porządkowe.
3. Dowodzenie terminacji programów za pomocą metod size-change termination.
4. Weryfikacja systemów czasu ciągłego z użyciem automatów czasowych.
5. Sprawdzanie stochastycznych modeli (ang. stochastic model-checking): weryfikacja dla łańcuchów Markowa czasu dyskretnego i ciągłego.
6. Sprawdzanie modeli nieskończeniestanowych: weryfikacja programów rekurencyjnych z użyciem automatów stosowych. Weryfikacja protokołów z kanałami komunikacyjnymi. Weryfikacja parametryzowana.
7. Sprawdzanie modeli dla hardware'u: weryfikacja układów kombinacyjnych i sekwencyjnych.
8. Synteza programów skończeniestanowych: problem Churcha i twierdzenie Büchi-Landwebera. Sterowanie Ramadge'a i Wonhama dla dyskretnych systemów zdarzeń.
Rodzaj przedmiotu
Założenia (lista przedmiotów)
Koordynatorzy przedmiotu
Efekty kształcenia
Wiedza: absolwent zna i rozumie
- w pogłębionym stopniu - wiedzę z działów matematyki niezbędnych do
studiowania informatyki (K_W01)
- w pogłębionym stopniu - rolę i znaczenie konstrukcji rozumowań
matematycznych (K_W02)
Umiejętności: absolwent potrafi
- konstruować rozumowania matematyczne (K_U01)
- wyrażać problemy obliczeniowe w języku matematyki (K_U02)
- analizować pojęcia sformalizowane w wybranych systemach logicznych o
znaczeniu informatycznym, tworzyć w nich formalizacje zadanych pojęć bądź
też dowodzić niemożności takiej formalizacji (K_U07)
Kryteria oceniania
Zaliczenie na podstawie prac domowych i końcowego egzaminu ustnego.
Literatura
Slajdy z wykładu i wybrane rozdziały następujących książek:
- Model Checking by Clarke, Grumberg, and Peled (1, 2)
- Principles of Model Checking by Baier and Katoen (1, 2, 4, 5)
- Handbook of Model Checking by Clarke, Henzinger, Veith, and Bloem (1, 2,
4, 5, 6, 8)
- Handbook of Automata Theory (8)
- Program termination analysis in polynomial time by Ben-Amram and Lee (3)
- Introduction to Formal Hardware Verification by Kropf (7)
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: