Skolan för
och kommunikation
KTH / CSC / Kurser / DD2457

Program Semantics and Analysis

Aktuell/nästa kursomgång: semant13.

Program Semantics and Analysis is a 6-point (högskolepoäng) course on the advanced level. It is coordinated together with its research-level version for doctoral students under the same name, but with course code DD3457.

To give a semantics for a programming language means to give a precise definition of the behaviour of programs written in this language. Only when the semantics of the language has been fixed, one can go about and prove such important properties like determinism and termination of program execution, equivalence of programs, correctness of translation of programs from one programming language into another, or that a program is correct. Different semantic styles have been developed for different purposes, depending on the level of detail needed for the particular task. The most important ones are: operational semantics, denotational semantics and axiomatic semantics.

The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, compare their strengths and weaknesses, and analyze how they can be used for establishing important properties of programming languages, concrete programs, and transformations on programs. A secondary goal is to learn the theories and proof techniques on which such semantic investigations are based.

The course is given in English. However, students can use Swedish when writing assignments and exams, and when communicating with the lecturer.


Course leader and lecturer:  Dilian Gurov, e-mail dilian at, phone 08-790 81 98.

Visiting address:  Osquars backe 2, floor 5, room 4520.

Copyright © Sidansvarig: Dilian Gurov <>
Uppdaterad 2012-10-30