Skip to main content

DD2457 Program Semantics and Analysis 6.0 credits

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.

Course offerings are missing for current or upcoming semesters.
Headings with content from the Course syllabus DD2457 (Spring 2022–) 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, program analysis and transformation.

* Part III. Axiomatic Semantics and Program Verification: axiomatic semantics, program specification and verification, weakest pre-conditions, verification condition generation.

Intended learning outcomes

The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, namely operational semantics, denotational semantics and axiomatic semantics, compare their strengths and weaknesses, and use these semantics for program analysis, optimisation and verification, both in theory and as a basis for software tools.

The successful student will be able to perform constructions such as:

* Construct the state space of a program as a basis for program behaviour analysis through state space exploration.

* Translate programs to abstract machine code, and execute the latter.

* Compute the denotation of a program.

* As above, but in abstract domains.

* Extend a programming language with new language features, and extend its semantics and abstract machine implementations accordingly.

* Suggest and justify program transformations supported by a suitable program analysis.

* Specify and verify programs in Hoare logic.

* Generate verification conditions from a program with annotated while loops.

as well as be able to formally establish results such as:

* Relate different semantic styles.

* Prove language properties such as determinism and termination.

* Show correctness of a given program transformation by proving equivalence of the original and the transformed program.

* Show properties of a given semantics.

For passing the course, a student has to demonstrate proficiency with problems of the first type; for the highest grade he/she has to be equally proficient at the remaining types of problems.

Literature and preparations

Specific prerequisites

Single course students:

DD1337 Programming, DD1338 Algorithms and Data Structures, SF1630 Discrete Mathematics, DD1350 Logic for Computer Scienceor corresponding courses.

Recommended prerequisites

5B1118/SF1610 Discrete Mathematics, mandatory and 5B1928/SF1642 Logic, recommended

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 - Exercises, 2.0 credits, grading scale: P, F
  • LAB1 - Laboratory Work, 2.0 credits, grading scale: P, F
  • TEN1 - Examination, 2.0 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.

Other requirements for final grade

* LAB1 - Laboratory work, 2,0 hp, grade: Pass/fail

* HEM1 - Exercises, 2,0 hp, grade: Pass/fail

* TEN1 - Examination, 2,0 hp, grade: A, B, C, D, E, FX, F

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

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

Main field of study

Computer Science and Engineering

Education cycle

Second cycle

Add-on studies

No information inserted

Contact

Dilian Gurov, e-post: dilian@kth.se, 790 8198

Transitional regulations

The examination is conducted during the transition period within the framework of the course DD2557. The course modules in DD2457 are replaced by course modules in DD2557 with the same name.