Conducted in terms: 2025/26_Z, 2026/27_Z

ECTS credits: 5

Language: Polish

Organized by: Faculty of Mathematics and Natural Sciences. School of Exact Sciences.

Semantics and the Verification of Software WM-I-S2-E1-SWP

This course introduces formal methods for describing and analyzing programs. It covers topics ranging from syntax and abstract syntax trees (ASTs) to an introduction to programming language semantics, including numerals, expressions, and state. Various semantic styles—such as natural semantics, structural operational semantics, abstract implementation, and abstract machines—are discussed in detail, alongside extensions covering control constructs.

Procedures and their description within static, dynamic, and combined semantics form a significant part of the course. Semantic approaches—including algebraic, axiomatic, denotational, and categorical (denotational and coalgebraic) methods—are also examined. Additionally, the semantics of domain-specific languages (DSLs) and concatenative languages are presented.

From a practical perspective, students learn to:
- construct abstract syntax trees,
- define semantic rules and prove properties of simple programs,
- derive a semantic language interpreter using the SLANG tool,
- analyze programs using Hoare logic and the fundamentals of the Chomsky hierarchy.

The course aims to provide mastery of both the theoretical foundations of program semantics and the practical skills required to apply formal methods to the verification of algorithms and programming languages.

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

information and communication technology

(in Polish) E-Learning

Term 2020/21_Z:

(in Polish) E-Learning (pełny kurs) z podziałem na grupy

Term 2021/22_Z:

(in Polish) E-Learning (pełny kurs) z podziałem na grupy

Term 2022/23_Z:

(in Polish) E-Learning (pełny kurs) z podziałem na grupy

Term 2023/24_Z:

(in Polish) E-Learning (pełny kurs) z podziałem na grupy

Term 2024/25_Z:

(in Polish) E-Learning

Term 2025/26_Z:

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

Term 2026/27_Z:

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

(in Polish) Grupa przedmiotów ogólnouczenianych

(in Polish) nie dotyczy

Course coordinators

Term 2026/27_Z:

Dorota Dąbrowska
William Steingartner

Term 2024/25_Z:

Dorota Dąbrowska
William Steingartner

Term 2023/24_Z:

Dorota Dąbrowska
William Steingartner

Term 2020/21_Z:

Term 2019/20_Z:

Term 2021/22_Z:

Term 2022/23_Z:

Term 2025/26_Z:

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

Term 2022/23_Z:

LECTURE Estimated student workload: - participation in classes 30 hours, - participation in the exam 1 hour, - 2-hour consultations with the tutor, - preparation for classes 5 hours, - preparation for the exam 14 hours, a total of 52 hours, which corresponds to 2 ECTS. LABORATORIES Estimated student workload: - participation in classes 30 hours, - consultations with the teacher 3 hours, - homework 30 hours, - preparation for verification 15 hours, in total 78 hours, which corresponds to 3 ECTS.

Term 2023/24_Z:

Term 2025/26_Z:

LECTURE Estimated student workload: - class participation: 30 hours, - exam participation: 2 hours, - consultations with the instructor: 3 hours, - class preparation: 5 hours, - exam preparation: 10 hours, total: 50 hours, equivalent to 2 ECTS. LABORATORIES Estimated student workload: - class participation: 30 hours, - consultations with the instructor: 3 hours, - homework: 10 hours, - class preparation: 5 hours, - assessment preparation: 12 hours, - project preparation: 15 hours, total: 75 hours, equivalent to 3 ECTS.

Term 2026/27_Z:

LECTURE Participation in classes: 30 hours Participation in examinations outside scheduled classes: 3 hours Participation in consultations: 4 hours Preparation for classes: 2 hours Preparation for the examination: 11 hours Total: 50 hours 1.5 ECTS – direct contact with the teacher 0.5 ECTS – independent study LABORATORY Participation in classes: 30 hours Participation in consultations: 4 hours Preparation for classes: 30 hours Preparation for assessment: 11 hours Total: 75 hours 1.4 ECTS – direct contact with the teacher 1.6 ECTS – independent study

Subject level

advanced

Learning outcome code/codes

lecture: I2_W01, I2_W05 laboratory: I2_U01, I2_U02, I2_U04, I2_U08, I2_K05 SYMBOL DESCRIPTIONS lecture - The graduate: I2_W01 - possesses in-depth knowledge and understanding of the theoretical foundations of computer science and information technologies, I2_W05 - possesses in-depth knowledge and understanding of methods for verifying program semantics, as well as concepts of program correctness and the techniques and formalisms used to prove it. laboratory - The graduate: I2_U01 - is able to apply mathematical methods for the analysis of algorithms and processes, I2_U02 - is able to apply mathematical and technical knowledge to formulate, analyze, and solve problems related to computer science, I2_U04 - is able to use formal semantics when reasoning about program correctness, I2_U08 - is able to determine directions for further learning and pursue self-study, I2_K05 - is prepared to think and act in a creative and entrepreneurial manner.

Type of subject

obligatory

Preliminary Requirements

Knowledge of the fundamentals of mathematical logic, discrete mathematics, and programming.

Learning outcomes

LECTURE

Student:
W1 – describes the theoretical foundations of the formal modeling and analysis of programs and computational processes (I2_W01),
W2 – characterizes various types of program semantics—operational, natural, denotational, algebraic, and axiomatic—and explains their application in program analysis (I2_W05),
W3 – characterizes methods for the formal verification of program properties and explains the concepts of program correctness and techniques for proving it (I2_W05).

LABORATORY

Student:
U1 – applies selected mathematical methods to the analysis of algorithms, computational processes, and program properties (I2_U01),
U2 – constructs and analyzes formal models of program execution, particularly using abstract machines (I2_U02),
U3 – employs various types of formal semantics to reason about program properties and correctness (I2_U04),
U4 – identifies knowledge gaps and independently expands their knowledge regarding program semantics and verification (I2_U08),
K1 – is prepared to independently and creatively seek solutions to problems in the field of program semantics and verification (I2_K05).

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-I-S2-E1-SWP in USOSweb