Formal Methods in Computer Science WM-MA-S1-MFI

This course introduces selected formal methods used in computer science and their mathematical foundations. It covers various models of computation—including automata, Turing machines, recursive functions, lambda calculus, term calculus, basic concepts of type theory, and selected logical systems—as well as the connections between these formalisms, programming languages, and methods of representing computation.

The course presents methods for formally describing program behavior, specifying program properties, and reasoning about correctness. It is complemented by selected models of concurrency, the fundamental concepts of category theory, and examples of their application in computer science.

The aim of the course is to familiarize students with various approaches to the mathematical and formal modeling of computation and to develop the ability to select and apply specific formal methods to the analysis of problems in computer science.

(in Polish) Dyscyplina naukowa, do której odnoszą się efekty uczenia się

mathematics

(in Polish) E-Learning

(in Polish) E-Learning (pełny kurs)

(in Polish) Grupa przedmiotów ogólnouczenianych

(in Polish) nie dotyczy

Course coordinators

Dorota Dąbrowska
William Steingartner

(in Polish) Opis nakładu pracy studenta w ECTS

LECTURE class attendance: 30 hours consultations: 4 hours class preparation: 16 hours preparation for assessment: 25 hours Total: 75 hours 1.4 ECTS – direct contact with the instructor 1.6 ECTS – independent work LABORATORY class attendance: 30 hours consultations: 4 hours class preparation and homework assignments: 30 hours preparation for assessment: 11 hours Total: 75 hours 1.4 ECTS – direct contact with the instructor 1.6 ECTS – independent work

Subject level

advanced

Learning outcome code/codes

(in Polish) wykład: MA1_W01, MA1_W04 ćwiczenia lub laboratorium: MA1_K01, MA1_K02, MA1_K07 OPIS SYMBOLI - Absolwent: wykład MA1_W01 - zna i rozumie cywilizacyjne znaczenie matematyki i jej zastosowań, MA1_W04 - zna i rozumie w zaawansowanym stopniu podstawowe twierdzenia z poznanych działów matematyki. ćwiczenia lub laboratorium MA1_K01 - jest gotów do identyfikacji ograniczeń własnej wiedzy i dalszego samokształcenia, MA1_K02 - jest gotów do formułowania pytań, służących pogłębieniu własnego zrozumienia danego tematu lub odnalezieniu brakujących elementów rozumowania, MA1_K07 - jest gotów do wyrażania opinii na temat podstawowych zagadnień matematycznych.

Type of subject

optional with unlimited choices

Preliminary Requirements

Basic knowledge of mathematical logic and discrete mathematics. Proficiency in programming in a chosen programming language.

Learning outcomes

LECTURE

The student:

W1 – knows and understands the mathematical foundations of selected formal models of computation, as well as their significance and application in computer science (MA1_W01, MA1_W04),

W2 – knows and understands the fundamental properties of selected logical formalisms, calculi, and type systems used to represent and analyze computations (MA1_W04),

W3 – knows and understands the application of mathematical methods to the formal description of program behavior, the specification of program properties, and reasoning about program correctness (MA1_W01, MA1_W04).

LABORATORY

The student:

K1 – is prepared to identify the limitations of their own knowledge and to independently expand it regarding the formal and mathematical foundations of computer science (MA1_K01),

K2 – is prepared to formulate questions and identify gaps in reasoning while analyzing formal models, program properties, and computational processes (MA1_K02),

K3 – is prepared to formulate and justify opinions regarding the application of selected mathematical and formal methods in computer science (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:

Description of WM-MA-S1-MFI in USOSweb