Weryfikacja wspomagana komputerowo
Informacje ogólne
Kod przedmiotu: | 1000-2N09WWK |
Kod Erasmus / ISCED: |
11.303
|
Nazwa przedmiotu: | Weryfikacja wspomagana komputerowo |
Jednostka: | Wydział Matematyki, Informatyki i Mechaniki |
Grupy: |
Przedmioty obieralne dla informatyki Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka |
Punkty ECTS i inne: |
(brak)
|
Język prowadzenia: | angielski |
Rodzaj przedmiotu: | monograficzne |
Założenia (lista przedmiotów): | Języki, automaty i obliczenia 1000-214bJAO |
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. |
Właścicielem praw autorskich jest Uniwersytet Warszawski.