Skip to main content
Till KTH:s startsida

DD2557 Program Semantics and Analysis 7.5 credits

Administer About course

To give a semantics for a programming language means to give a precise definition of the behaviour of programs written in this language. Once the semantics of the language has been described formally, one can go about and prove various language properties like determinism, prove correctness of program implementations based on abstract machines, justify various program analyses used in syntax-oriented editors and program transformations used in optimising compilers, and specify and prove correctness of concrete programs. This provides the formal basis for a variety of software tools for program analysis, optimisation and verification.

Information per course offering

Termin

Information for Spring 2025 semant25 programme students

Course location

KTH Campus

Duration
17 Mar 2025 - 2 Jun 2025
Periods
P4 (7.5 hp)
Pace of study

50%

Application code

60440

Form of study

Normal Daytime

Language of instruction

English

Course memo
Course memo is not published
Number of places

Min: 15

Target group

Open to students admitted to a master's programme as long as the course can be included in the programme.

Planned modular schedule
[object Object]
Schedule
Schedule is not published

Contact

Examiner
No information inserted
Course coordinator
No information inserted
Teachers
No information inserted

Course syllabus as PDF

Please note: all information from the Course syllabus is available on this page in an accessible format.

Course syllabus DD2557 (Spring 2023–)
Headings with content from the Course syllabus DD2557 (Spring 2023–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

Part I. Operational semantics and language implementation: natural semantics, structural operational semantics, abstract machines, correctness of language implementation.

Part II. Denotational semantics and program analysis: denotational semantics, fixed point theory, abstract interpretation, program analysis and program transformation.

Part III. Axiomatic semantics and program verification: axiomatic semantics, program specification and verification, weakest preconditions, verification condition generation.

Intended learning outcomes

After passing the course, the student should be able to

  • construct the state space of a program as a basis for program behaviour analysis
  • translate programs to abstract machine code and execute it
  • compute the denotation of a program
  • extend a programming language with new language features, and extend its semantics and abstract machine implementations accordingly
  • suggest and justify program transformations supported by an appropriate program analysis
  • specify and verify programs in Hoare logic
  • generate verification conditions of a given program and specification
  • relate different semantic styles formally 
  • prove language properties such as determinism and termination formally 
  • prove the correctness of a given program transformation by showing equivalence between the original program and the transformed program formally
  • show properties of a given semantics formally.

Literature and preparations

Specific prerequisites

Knowledge and skills in programming, 5 credits, equivalent to completed course DD1337/DD1310-DD1318/DD1321/DD1331/DD100N/ID1018.

Knowledge in basic computer science, 6 credits, equivalent to completed course DD2325/DD1320/DD1325/DD1327/DD2325/ID1020/ID1021.

Knowledge in discrete mathematics, 6 higher education credits, equivalent to completed course SF1688/SF1610/SF1630/SF1662/SF1679.

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale

A, B, C, D, E, FX, F

Examination

  • HEM1 - Home assignments, 2.5 credits, grading scale: P, F
  • LAB1 - Laboratory work, 2.5 credits, grading scale: P, F
  • TEN1 - Home exam, 2.5 credits, grading scale: A, B, C, D, E, FX, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

Profile picture Dilian Gurov

Ethical approach

  • All members of a group are responsible for the group's work.
  • In any assessment, every student shall honestly disclose any help received and sources used.
  • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

Further information

Course room in Canvas

Registered students find further information about the implementation of the course in the course room in Canvas. A link to the course room can be found under the tab Studies in the Personal menu at the start of the course.

Offered by

EECS/Computer Science

Main field of study

Computer Science and Engineering

Education cycle

Second cycle

Add-on studies

No information inserted

Supplementary information

In this course, the EECS code of honor applies, see:
http://www.kth.se/en/eecs/utbildning/hederskodex