Formal methods in computer science WM-MA-S1-E5-MFWI
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 2023/24_Z: (in Polish) E-Learning | Term 2024/25_Z: (in Polish) E-Learning | 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) udział w zajęciach, 60h
nauka własna, 40h,
przygotowanie projektów informatycznych, 50h
w sumie 150h czyli 6ECTS | Term 2022/23_Z: (in Polish) udział w zajęciach, 60h
nauka własna, 40h,
przygotowanie projektów informatycznych, 50h
w sumie 150h czyli 6ECTS | 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
Preliminary Requirements
Course coordinators
Term 2023/24_Z: | Term 2025/26_Z: | Term 2024/25_Z: | Term 2022/23_Z: |
Learning outcomes
Lecture
W1 - Understands the importance of formal methods in software validation (MA1_W01),
W2 - Knows the basic theorems concerning the semantics of programming languages and Hoare's logic (MA1_W04).
Lab Courses
L1 - Is ready to develop their knowledge of software validation (MA1_K01),
L2 - Is ready to detect missing elements in software formalization (MA1_K02),
L3 - Is ready to evaluate the correctness of software formalization (MA1_K07).
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: