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.
FDD3557 Program and Semantics and Analysis 7.5 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.
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 FDD3557 (Spring 2023–)Information for research students about course offerings
The course is offered every other year in period 4.
Headings with content from the Course syllabus FDD3557 (Spring 2023–) are denoted with an asterisk ( )
Content and learning outcomes
Course disposition
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:
- Account for the main semantic styles used for capturing the meaning of programs in a formal way, both in theory and on examples.
- Relate different semantic styles, and compare their strengths and weaknesses.
- Use these semantic styles for program analysis, optimisation and verification, both in theory and as a basis for software tools.
- Extend a programming language with new language features, and extend its semantics accordingly.
- Prove formally properties of a given semantics.
Literature and preparations
Specific prerequisites
No information inserted
Recommended prerequisites
Courses in Programming, Discrete Mathematics, and Mathematical Logic.
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, 7.5 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
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
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)