Semantics and the Verification of Software WM-I-S2-E1-SWP
This course provides an introduction to formal methods for program description and analysis. It covers topics ranging from syntax and abstract syntax trees (ASTs), through an introduction to the semantics of programming languages, including numerals, expressions, and state. Various styles of semantics are discussed in detail: natural, structured operational, abstract implementation, and abstract machines, as well as extensions of semantics to include control constructs.
Procedures and their description in static, dynamic, and combined semantics constitute an important part of the course. Algebraic, axiomatic, denotative, and categorical (denotative and co-algebraic) semantic approaches are also discussed. Additionally, the semantics of domain-specific languages (DSLs) and concatenative languages are presented.
From a practical perspective, students learn:
- construct abstract syntax trees,
- define semantic rules and prove properties of simple programs,
- generate a semantic language interpreter using SLANG,
- analyze programs using Hoare logic and the basics of Chomsky hierarchy.
The course aims to master both the theoretical foundations of program semantics and the practical application of formal methods to verify the correctness of algorithms and programming languages.
(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 2022/23_Z: (in Polish) E-Learning (pełny kurs) z podziałem na grupy | Term 2020/21_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: 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 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 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. |
Subject level
Learning outcome code/codes
Type of subject
Preliminary Requirements
Course coordinators
Term 2023/24_Z: | Term 2019/20_Z: | Term 2021/22_Z: | Term 2020/21_Z: | Term 2022/23_Z: | Term 2024/25_Z: | Term 2025/26_Z: |
Learning outcomes
LECTURE
Student:
W1 - knows and understands the basics of the theory of formal languages and automata with applications (I2_W01),
W2 - knows and understands various types of program semantics and methods of program ownership verification (I2_W05),
W3 - knows and understands the concepts related to the correctness of programs and selected techniques and formalisms of proving the correctness of algorithms and programs (I2_W05).
LABORATORIES
Student:
U1 - can use selected mathematical methods to analyze the correctness of algorithms (I2_U01),
U2 - can build abstract machines and analyze their operation (I2_U02),
U3 - can use various types of formal semantics to infer about the properties of programs (I2_U04),
U4 - can learn independently (I2_U08),
K1 - is ready to actively participate in the laboratory and creatively solve problems (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: