Metody formalne w informatyce-zajęcia fakultatywne
Informacje ogólne
Kod przedmiotu: | WM-MA-S1-E5-MFWI |
Kod Erasmus / ISCED: | (brak danych) / (brak danych) |
Nazwa przedmiotu: | Metody formalne w informatyce-zajęcia fakultatywne |
Jednostka: | Wydział Matematyczno-Przyrodniczy. Szkoła Nauk Ścisłych |
Grupy: | |
Punkty ECTS i inne: |
6.00
|
Język prowadzenia: | polski |
Dyscyplina naukowa, do której odnoszą się efekty uczenia się: | matematyka |
Poziom przedmiotu: | zaawansowany |
Symbol/Symbole kierunkowe efektów uczenia się: | wykład MA1_W01, MA1_W04 laboratoria MA1_K01, MA1_K02, MA1_K07 |
Wymagania wstępne: | Znajomość podstaw matematyki i logiki matematycznej. Umięjtność programowania w wybranym języku programowania. |
Pełny opis: |
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. |
Efekty kształcenia i opis ECTS: |
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). |
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ą 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 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: | Konrad Zdanowski | |
Prowadzący grup: | Konrad Zdanowski | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: |
Przedmiot -
Egzaminacyjny
Laboratorium - Zaliczenie na ocenę Wykład - Egzaminacyjny |
|
E-Learning: | E-Learning (pełny kurs) z podziałem na grupy |
|
Opis nakładu pracy studenta w ECTS: | udział w zajęciach, 60h nauka własna, 40h, przygotowanie projektów informatycznych, 50h w sumie 150h czyli 6ECTS |
|
Literatura: |
Literatura podstawowa Ben-Ari, Logika dla informatyków, WNT. Literatura uzupełniająca Yves Bertot, Coq in hurry, 2017, url: https://hal.inria.fr/inria-00001173/en/ Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program De- velopment, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004. url: http://www.labri.fr/Perso/%7Ecasteran/CoqArt/index.html Francois Bobot et al., The Why3 platform, 2022, url: https://why3.lri.fr/doc/ |
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: | Konrad Zdanowski | |
Prowadzący grup: | Konrad Zdanowski | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Egzaminacyjny | |
E-Learning: | E-Learning |
|
Opis nakładu pracy studenta w ECTS: | udział w zajęciach, 60h nauka własna, 40h, przygotowanie projektów informatycznych, 50h w sumie 150h czyli 6ECTS |
|
Typ przedmiotu: | obowiązkowy |
|
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.