Metody formalne w informatyce - zajecia specjalnościowe WM-I-S1-E5-MFI
Przedmiot stanowi wprowadzenie w formalne metody analizy programów, dowodzenia własności programów oraz w wykorzystania 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.
Dyscyplina naukowa, do której odnoszą się efekty uczenia się
E-Learning
W cyklu 2024/25_Z: E-Learning | W cyklu 2023/24_Z: E-Learning (pełny kurs) z podziałem na grupy | W cyklu 2022/23_Z: E-Learning (pełny kurs) z podziałem na grupy | W cyklu 2021/22_Z: E-Learning (pełny kurs) z podziałem na grupy |
Grupa przedmiotów ogólnouczenianych
Opis nakładu pracy studenta w ECTS
W cyklu 2023/24_Z: Wykład
udział w zajęciach, 30h
nauka własna zagadnień z wykładu, 20h,
studia nad literaturą, 25h,
suma: 75h (3 p. ECTS)
Laboratoria
udział w zajęciach, 30h,
nauka własna, 20h,
przygotowanie projektów informatycznych, 30h
Suma: 80h (3 p. ECTS) | W cyklu 2022/23_Z: Wykład
udział w zajęciach, 30h
nauka własna zagadnień z wykładu, 20h,
studia nad literaturą, 25h,
Suma: 75h (3 p. ECTS),
Laboratoria
udział w zajęciach, 30h,
nauka własna, 20h,
przygotowanie projektów informatycznych, 30h
Suma: 80h (3 p. ECTS) |
Poziom przedmiotu
Symbol/Symbole kierunkowe efektów uczenia się
Typ przedmiotu
W cyklu 2023/24_Z: fakultatywny ograniczonego wyboru | W cyklu 2024/25_Z: obowiązkowy | W cyklu 2022/23_Z: fakultatywny ograniczonego wyboru |
Wymagania wstępne
Koordynatorzy przedmiotu
W cyklu 2023/24_Z: | W cyklu 2024/25_Z: | W cyklu 2022/23_Z: | W cyklu 2021/22_Z: |
Efekty kształcenia
Wykład:
W1 - student zna zasady formalizacji własności programów oraz rozumie ich semantykę (I1_W14),
U1 - student zna programy ułatwiające weryfikację oprogramowania oraz teorie formalne, na których się opierają (I1_U18),
Laboratoria:
W1 - student zna narzędzia informatyczne służące do automatycznej weryfikacji programów (I1_W14),
U1 - student potrafi wykorzystać wybrane narzędzia informatyczne, aby udowodnić poprawność zaprogramowanych funkcji (I1_U18)
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ą.
Więcej informacji
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: