University of Warsaw - Central Authentication System
Strona główna

Program semantics and verification

General data

Course ID: 1000-215bSWP
Erasmus code / ISCED: 11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title: Program semantics and verification
Name in Polish: Semantyka i weryfikacja programów
Organizational unit: Faculty of Mathematics, Informatics, and Mechanics
Course groups: Obligatory courses for 3rd grade Computer Science
Obligatory courses for 3rd grade JSIM (3I+4M)
Obligatory courses for 3rd grade JSIM (3M+4I)
Course homepage: http://www.mimuw.edu.pl/~tarlecki/teaching/semwer/
ECTS credit allocation (and other scores): 5.00 Basic information on ECTS credits allocation principles:
  • the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS;
  • the student’s weekly hourly workload is 45 h;
  • 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes;
  • weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS;
  • work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load.
view allocation of credits
Language: Polish
Type of course:

obligatory courses
Requirements:

Foundations of mathematics 1000-211bPM
Introductory programming 1000-211bWPI
Languages, automata and computations 1000-214bJAO
Mode:

Classroom
Short description:

The aim of the course is to present the importance as well as basic problems and techniques of formal description of programs. Various methods of defining program semantics are discussed, and their mathematical foundations as well as techniques are presented. The basic notions of program correctness are introduced together with methods and formalisms for their derivation.

Full description:

1. Formal description of programming languages

2. Operational and denotational methods of program semantics definition

3. Semantic definitions of basic programming constructs

4. Mathematical underpinnings of denotational semantics

5. Basic notions of program correctness: partial and total correctness

6. Proof methods for program correctness

7. Hoare's logic, its application and formal properties

8. Basic notions of universal algebra and their role in programming language descriptions

Prerequisities:

- Introductory programming (1000-211bWPI and/or 1000bWPF)

- Foundations of mathematics (1000-211bPM)

- Languages, automata and computations (1000-214bJAO)
Bibliography:

1. M. Hennessy. The Semantics of Programming Languages. Wiley, 1990.

2. M. Fernandez. Programming Languages and Operational Semantics: An Introduction. College Publications, 2004.

3. H. Riis Nielson, F. Nielson. Semantics with Applications: An Appetizer. Springer, 2007.

4. M. Gordon. The Denotational Description of Programming Languages. Springer-Verlag, 1979.

5. D. Gries. The Science of Programming. Springer-Verlag, 1981.

6. E. Dijkstra. A Discipline of Programming. Prentice-Hall 1976.
Learning outcomes:

Knowledge. Students know and understand:

- the concepts of syntax and semantics of programming languages, methods of defining them, and definitions of simple programming constructs (K_W02, K_W03, K_W13);

- mathematical foundations of defining semantics of programming languages (K_W13);

- the notion of program correctness with respect to a formal specification (K_W02, K_W04, K_W13);

- formal methods of proving partial and total correctness of simple programs (K_W04, K_W10, K_W13).

Skills. Students are able to:

- define semantics of simple programming constructs and understand the working of programming constructs from their semantic descriptions (K_U01, K_U03);

- apply formal verification methods to prove correctness of simple programs (K_U03,K_U07);

- justify the correctness of programs referring to their semantics (K_U03).

Competence. Students are ready to:

- know the limits of their knowledge and understand the need of further education (K_K01)

- understand and appreciate the importance of precision and rigour in formulating problems and justifying the correctness of their solutions (K_K03).
Assessment methods and assessment criteria:

Final grade based on a written exam and homework exercises given during the semester.

Classes in period "Winter semester 2023/24" (past)

Time span: 2023-10-01 - 2024-01-28
Selected timetable range:
Navigate to timetable
Type of class:
Classes, 30 hours more information
Lecture, 30 hours more information
Coordinators: Andrzej Tarlecki
Group instructors: Ewa Madalińska-Bugaj, Aleksy Schubert, Michał Skrzypczak, Andrzej Tarlecki
Students list: (inaccessible to you)
Examination: Examination
Course descriptions are protected by copyright.
Copyright by University of Warsaw.
Krakowskie Przedmieście 26/28
00-927 Warszawa tel: +48 22 55 20 000 https://uw.edu.pl/ contact accessibility statement USOSweb 7.0.3.0 (2024-03-22)