FDD3457 Program and Semantics ans Analysis 6.0 credits

Programsemantik och programanalys

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.

Offering and execution

Course offering missing for current semester as well as for previous and coming semesters

Course information

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.

Course Disposition

The course consist of lectures, lab sessions, a seminar and a written final exam. There are six homeworks, which are peer-reviewed in class, and two laboratory assignments.

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

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 web

Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.

Course web FDD3457

Offered by

EECS/Theoretical Computer Science

Main field of study *

No information inserted

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