Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

Weryfikacja wspomagana komputerowo

Informacje ogólne

Kod przedmiotu: 1000-2N09WWK
Kod Erasmus / ISCED: 11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
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) Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.

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.

Przedmiot nie jest oferowany w żadnym z aktualnych cykli dydaktycznych.
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.
Krakowskie Przedmieście 26/28
00-927 Warszawa
tel: +48 22 55 20 000 https://uw.edu.pl/
kontakt deklaracja dostępności USOSweb 7.0.3.0 (2024-03-22)