Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie - Centralny System Uwierzytelniania
Strona główna

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) 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: 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
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
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
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
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
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
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
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
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

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie.
ul. Dewajtis 5,
01-815 Warszawa
tel: +48 22 561 88 00 https://uksw.edu.pl
kontakt deklaracja dostępności mapa serwisu USOSweb 7.1.0.0-8 (2024-11-08)