Skip to main content
Till KTH:s startsida

FDD3457 Program and Semantics and Analysis 6.0 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

Course offerings are missing for current or upcoming semesters.

Course syllabus as PDF

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

Course syllabus FDD3457 (Spring 2019–)
Headings with content from the Course syllabus FDD3457 (Spring 2019–) 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

After completing the course, the successful doctoral student should be able to:

  1. Account for the main semantic styles used for capturing the meaning of programs in a formal way, both in theory and on examples.
  2. Relate different semantic styles, and compare their strengths and weaknesses.
  3. Use these semantic styles for program analysis, optimisation and verification, both in theory and as a basis for software tools.
  4. Extend a programming language with new language features, and extend its semantics accordingly.
  5. Prove formally properties of a given semantics.

Literature and preparations

Specific prerequisites

No information inserted

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9. Research papers.

Examination and completion

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

Grading scale

P, F

Examination

  • EXA1 - Examination, 6.0 credits, grading scale: P, 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

To pass the course, doctoral students need to pass the homework assignments, the laboratory assignments, the seminar, and the written exam.

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/Theoretical Computer Science

Main field of study

This course does not belong to any Main field of study.

Education cycle

Third cycle

Add-on studies

No information inserted

Contact

Dilian Gurov (dilian@kth.se)

Postgraduate course

Postgraduate courses at EECS/Theoretical Computer Science