Program Semantics and Verification 1000-2M24SWP
The lectures cover the following topics:
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
The laboratory classes illustrate the use of such methods in the practical design and implementation of programming languages and program verification. Students will have the opportunity to implement their own programming language. This will be carried out within (small) group projects that involve designing a simple programming language, then defining its formal semantics and implementing its interpreter based on this semantics, further complemented by practical examples of program verification supported by existing verification and proof systems.
Type of course
Prerequisites
Course coordinators
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);
- applications of these methods in the process of software design and implementation (K_W02, K_W03, 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 and their practical use involving support verification and proof tools (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 for 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 criteria
Final grade based on a written exam and the lab projects carried out during the semester.
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: An Introduction. Springer-Verlag, 1979.
5. K. R. Apt, Ten Years of Hoare’s Logic: A Survey — Part 1, ACM Toplas 3(4), 1981, 431-483.
6. E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
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:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: