Semantics and the Verification of Software WM-I-SWP

As part of the course, students will be familiarized with the methods of formal description of algorithms (programs). Natural, denotational and operational semantics will be presented. The basis for these considerations will be an introduction to automata theory, formal languages and computations. Students will become familiar with the basic structures and algorithms of this theory. The Chomsky's hierarchy will be presented. Properties of algorithms (programs) and methods of their verification will be presented on appropriate examples.

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

information and communication technology

(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) nie dotyczy

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

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.

Subject level

advanced

Learning outcome code/codes

Lecture: I2_W01, I2_W05; laboratories: I2_U01, I2_U02, I2_U04, I2_U08, I2_K05

Type of subject

obligatory

Preliminary Requirements

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

Course coordinators

Term 2023/24_Z:

Dorota Dąbrowska
William Steingartner

Term 2019/20_Z:

Term 2021/22_Z:

Term 2020/21_Z:

Term 2022/23_Z:

Term 2024/25_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

Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:

Computer Science - full-time second-cycle studies

Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system:

Description of WM-I-SWP in USOSweb