Metody formalne w informatyce - zajecia specjalnościowe
Informacje ogólne
Kod przedmiotu: | WM-I-S1-E5-MFI |
Kod Erasmus / ISCED: | (brak danych) / (brak danych) |
Nazwa przedmiotu: | Metody formalne w informatyce - zajecia specjalnościowe |
Jednostka: | Wydział Matematyczno-Przyrodniczy. Szkoła Nauk Ścisłych |
Grupy: | |
Punkty ECTS i inne: |
0 LUB
6.00
(w zależności od programu)
|
Język prowadzenia: | polski |
Dyscyplina naukowa, do której odnoszą się efekty uczenia się: | informatyka techniczna i telekomunikacja |
Poziom przedmiotu: | zaawansowany |
Symbol/Symbole kierunkowe efektów uczenia się: | wykład I1_W14, I1_U18 laboratoria I1_W14, I1_U18 |
Wymagania wstępne: | Znajomość podstaw logiki matematycznej, rachunku zdań i logiki pierwszego rzędu. Umiejętność programowania w wybranym języku. |
Pełny opis: |
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. |
Efekty kształcenia i opis ECTS: |
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) |
Metody i 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ą. |
Zajęcia w cyklu "Semestr zimowy 2021/22" (zakończony)
Okres: | 2021-10-01 - 2022-01-31 |
Przejdź do planu
PN WYK
LAB
WT ŚR CZ PT |
Typ zajęć: |
Laboratorium, 30 godzin
Wykład, 30 godzin
|
|
Koordynatorzy: | Konrad Zdanowski | |
Prowadzący grup: | Konrad Zdanowski | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzaminacyjny | |
E-Learning: | E-Learning (pełny kurs) z podziałem na grupy |
Zajęcia w cyklu "Semestr zimowy 2022/23" (zakończony)
Okres: | 2022-10-01 - 2023-01-31 |
Przejdź do planu
PN WT ŚR CZ PT WYK
LAB
|
Typ zajęć: |
Laboratorium, 30 godzin
Wykład, 30 godzin
|
|
Koordynatorzy: | Dorota Dąbrowska, Konrad Zdanowski | |
Prowadzący grup: | Konrad Zdanowski | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzaminacyjny | |
E-Learning: | E-Learning (pełny kurs) z podziałem na grupy |
|
Opis nakładu pracy studenta w ECTS: | 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) |
|
Typ przedmiotu: | fakultatywny ograniczonego wyboru |
Zajęcia w cyklu "Semestr zimowy 2023/24" (zakończony)
Okres: | 2023-10-01 - 2024-01-31 |
Przejdź do planu
PN WT ŚR CZ WYK
LAB
PT |
Typ zajęć: |
Laboratorium, 30 godzin
Wykład, 30 godzin
|
|
Koordynatorzy: | Dorota Dąbrowska, Konrad Zdanowski | |
Prowadzący grup: | Konrad Zdanowski | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzaminacyjny | |
E-Learning: | E-Learning (pełny kurs) z podziałem na grupy |
|
Opis nakładu pracy studenta w ECTS: | 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) |
|
Typ przedmiotu: | fakultatywny ograniczonego wyboru |
|
Grupa przedmiotów ogólnouczenianych: | nie dotyczy |
Zajęcia w cyklu "Semestr zimowy 2024/25" (zakończony)
Okres: | 2024-10-01 - 2025-01-31 |
Przejdź do planu
PN WT ŚR CZ PT WYK
LAB
|
Typ zajęć: |
Laboratorium, 30 godzin
Wykład, 30 godzin
|
|
Koordynatorzy: | William Steingartner | |
Prowadzący grup: | William Steingartner | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzaminacyjny | |
E-Learning: | E-Learning |
|
Typ przedmiotu: | obowiązkowy |
|
Grupa przedmiotów ogólnouczenianych: | nie dotyczy |
Właścicielem praw autorskich jest Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie.