Metody formalne w informatyce-zajęcia fakultatywne WM-MA-S1-E5-MFWI
Przedmiot stanowią wprowadzenie w formalne metody analizy programów, dowodzenie własności programów oraz w wykorzystanie automatycznych metod przeprowadzenia takiej analizy jak SAT solwery oraz systemy automatycznego dowodzenia. Słuchacze podczas kursu poznają metody dowodzenia w rachunku zdań i logice pierwszego rzędu, nauczą się semantyki programów, analizować kod programu za pomocą logiki Hoare'a oraz dowodzić własności programu. Ponadto, poznają narzędzia pozwalające zautomatyzować ten proces.
Celem kursu jest zapoznanie słuchacza z wymienionymi wyżej technikami. Po jego ukończeniu student powinien być w stanie korzystać z asystentów automatycznego dowodzenia, powinien rozumieć dowody poprawności algorytmów, powinien potrafić formułować warunki poprawności danego algorytmu i weryfikować poprawność prostych algorytmów.
Dyscyplina naukowa, do której odnoszą się efekty uczenia się
E-Learning
W cyklu 2023/24_Z: E-Learning | W cyklu 2024/25_Z: E-Learning | W cyklu 2022/23_Z: E-Learning (pełny kurs) z podziałem na grupy |
Grupa przedmiotów ogólnouczenianych
Opis nakładu pracy studenta w ECTS
Poziom przedmiotu
Symbol/Symbole kierunkowe efektów uczenia się
Typ przedmiotu
Wymagania wstępne
Koordynatorzy przedmiotu
W cyklu 2024/25_Z: | W cyklu 2023/24_Z: | W cyklu 2022/23_Z: |
Efekty kształcenia
Wykład
W1 - rozumie znaczenie metod formalnych w weryfikacji poprawności oprogramowania (MA1_W01),
W2 - zna podstawowe twierdzenia dotyczące semantyki języków programowania i logiki Hoare'a (MA1_W04).
Laboratoria
L1 - jest gotowy do rozwoju swojej wiedzy z dziedziny weryfikacji oprogramowania (MA1_K01),
L2 - jest gotowy do wykrywania brakujących elementów w formalizacji oprogramowania (MA1_K02),
L3 - jest gotowy do opiniowania poprawności formalizacji oprogramowania (MA1_K07).
Kryteria oceniania
Dla wszystkich efektów przyjmuje się następujące kryteria oceny we wszystkich formach weryfikacji:
ocena 5: osiągnięty w pełni (bez uchwytnych niedociągnięć)
ocena 4,5: osiągnięty niemal w pełni i nie są spełnione kryteria przyznania wyższej oceny
ocena 4: osiągnięty w znacznym stopniu i nie są spełnione kryteria przyznania wyższej oceny
ocena 3,5: osiągnięty w znacznym stopniu
z wyraźną przewagą pozytywów i nie są spełnione kryteria
przyznania wyższej oceny
ocena 3: osiągnięty dla większości przypadków objętych weryfikacją i nie są spełnione kryteria przyznania
wyższej oceny
ocena 2: nie został osiągnięty dla większości przypadków objętych weryfikacją
wyższej oceny
ocena 2: nie został osiągnięty dla większości przypadków objętych weryfikacją
Więcej informacji
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: