Uniwersytet Warszawski - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Weryfikacja wspomagana komputerowo

Informacje ogólne

Kod przedmiotu: 1000-2N09WWK Kod Erasmus / ISCED: 11.303 / (0612) Database and network design and administration
Nazwa przedmiotu: Weryfikacja wspomagana komputerowo
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty monograficzne dla III - V roku informatyki
Przedmioty obieralne dla informatyki
Przedmioty obieralne stałe dla informatyki
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: angielski
Rodzaj przedmiotu:

monograficzne

Założenia (lista przedmiotów):

Języki, automaty i obliczenia 1000-214bJAO
Podstawy matematyki 1000-211bPM

Tryb prowadzenia:

w sali

Skrócony opis:

Metody automatycznej weryfikacji systemów komputerowych (oprogramowania lub układów sprzętowych): weryfikacja modelowa (ang. model checking), analiza statyczna, dowodzenie poprawności programów.

Podstawy teoretyczne, złożoność obliczeniowa, algorytmy, narzędzia.

Metody walki z tzw. eksplozją stanów: podejścia symboliczne, metody abstrakcji, redukcje liczby stanów. Interpretacja abstrakcyjna. Języki specyfikacji własności programów i dowodzenie poprawności. Mechanizmy generowania programów.

Na laboratorium zapoznajemy się z wybranymi narzędziami (np. SMV, SPIN, CBMC, UPPAAL, Coq, Why) i z ich praktycznymi zastosowaniami.

Pełny opis:

1. Wprowadzenie do weryfikacji wspomaganej komputerowo, historia dziedziny (1 wykład)

2. Logiki temporalne czasu liniowego i rozgałęzionego: LTL, CTL, CTL* (1-2 wykłady)

3. Weryfikacja modelowa (ang. model-checking): złożoność, algorytmy globalne i lokalne (w locie), omega-automaty, SPIN i język specyfikacji Promela, metody redukcji rozmiaru przestrzeni stanów (2-3 wykłady)

4.Podejścia symboliczne: weryfikacja symboliczna przy użyciu OBDD, ograniczona weryfikacja modelowa (ang. bounded model checking), zastosowanie SAT-solvera, SMV, CBMC (2-3 wykłady)

5. Metody abstrakcji, uszczegóławianie na podstawie kontrprzykładu (ang. CEGAR) (1-2 wykłady)

6. Wybrane metody analizy statycznej programów, interpretacja abstrakcyjna (ang. abstract interpretation) i jej zastosowania (2-3 wykłady)

7. Języki specyfikacji własności programów, dowodzenie poprawności programów przy użyciu, np. systemu wspomagania dowodzenia Coq i platformy do weryfikacji programów Why, mechanizmy generowania programów (2-3 wykłady)

8. (opcjonalnie) Weryfikacja systemów probabilistycznych i zależnych od czasu, UPPAAL (2 wykłady)

Literatura:

1. E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, MIT Press, 2002.

2. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, P. McKenzie, Systems and Software Verification, Springer, 2001.

3. C. Baier, J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.

4. G. J. Holzmann, The SPIN Model Checker. Pearson Educational, 2003.

5. F. Nielson, H.R. Nielson, C. Hankin, Principles of Program Analysis, Springer, 2005.

Efekty uczenia się:

Wiedza

1. Ma uporządkowaną, podbudowaną teoretycznie wiedzę ogólną w zakresie algorytmów i złożoności dotyczących weryfikacji modelowej (K_W02)

2. Ma ogólną wiedzę w zakresie dowodzenia poprawności programów przy użyciu systemów wspomagania dowodzenia (K_W02)

Umiejętności

1. Potrafi pisać, uruchamiać i weryfikować własności programów w wybranym środowisku programistycznym (K_U05)

2. Potrafi pozyskiwać informacje z literatury, Internetu oraz innych wiarygodnych źródeł, integrować je, dokonywać ich interpretacji (K_U02)

Kompetencje

1. Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia (K_K01)

2. Potrafi samodzielnie wyszukiwać informacje w literaturze, także w językach obcych (K_K05)

Metody i kryteria oceniania:

Ocena końcowa na podstawie punktów z egzaminu pisemnego i programów zaliczeniowych.

Zajęcia w cyklu "Semestr letni 2019/20" (zakończony)

Okres: 2020-02-17 - 2020-08-02
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium więcej informacji
Wykład więcej informacji
Koordynatorzy: Aleksy Schubert
Prowadzący grup: Aleksy Schubert, Jakub Zakrzewski
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin

Zajęcia w cyklu "Semestr letni 2020/21" (jeszcze nie rozpoczęty)

Okres: 2021-02-22 - 2021-06-13
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Bartosz Klin
Prowadzący grup: Bartosz Klin
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.