Formal methods in computer science WM-I-S1-E5-MFI
This course introduces fundamental formal methods in computer science: automata, Turing machines, recursive functions, lambda calculus, and term calculus. It also includes an introduction to the semantics of programming languages in various approaches (denotative, algebraic, axiomatic), logical and concurrent models, and selected applications of category theory. The course aims to develop skills in formal program analysis, proving their properties, and understanding models of computation.
(in Polish) Dyscyplina naukowa, do której odnoszą się efekty uczenia się
(in Polish) E-Learning
Term 2021/22_Z: (in Polish) E-Learning (pełny kurs) z podziałem na grupy | Term 2024/25_Z: (in Polish) E-Learning | Term 2023/24_Z: (in Polish) E-Learning (pełny kurs) z podziałem na grupy | Term 2025/26_Z: (in Polish) E-Learning (pełny kurs) | Term 2022/23_Z: (in Polish) E-Learning (pełny kurs) z podziałem na grupy |
(in Polish) Grupa przedmiotów ogólnouczenianych
(in Polish) Opis nakładu pracy studenta w ECTS
Term 2023/24_Z: (in Polish) 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) | Term 2022/23_Z: (in Polish) 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) | Term 2025/26_Z: Lecture
class participation, 30 hours
independent study of lecture topics, 20 hours
literature studies, 25 hours
total: 75 hours (3 ECTS points)
Laboratories
class participation, 30 hours
independent study, 20 hours
computer projects preparation, 25 hours
total: 75 hours (3 ECTS points) |
Subject level
Learning outcome code/codes
Type of subject
Term 2023/24_Z: optional with limited choices | Term 2024/25_Z: obligatory | Term 2025/26_Z: optional with limited choices | Term 2022/23_Z: optional with limited choices |
Preliminary Requirements
Course coordinators
Term 2021/22_Z: | Term 2023/24_Z: | Term 2024/25_Z: | Term 2025/26_Z: | Term 2022/23_Z: |
Learning outcomes
Lecture:
W1 - The student knows the principles of formalizing program properties and understands their semantics (I1_W14),
U1 - The student knows programs that facilitate software verification and the formal theories on which they are based (I1_U18),
Laboratory:
W1 - The student knows IT tools for automatic program verification (I1_W14),
U1 - The student can use selected IT tools to prove the correctness of programmed functions (I1_U18)
Assessment criteria
For all learning outcomes, the following assessment criteria are adopted for all forms of verification:
grade 5: fully achieved (no obvious shortcomings),
grade 4.5: achieved almost fully and criteria for awarding a higher grade are not met,
grade 4: largely achieved and the criteria for a higher grade are not met,
grade 3.5: largely achieved - with a clear majority of positives - and the criteria for granting a higher grade are not met,
grade 3: achieved for most of the cases covered by the verification and criteria for a higher grade are not met,
grade 2: not achieved for most of the cases covered by the verification.
Additional information
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: