FDD3457 Program and Semantics and Analysis 6.0 credits
This course has been discontinued.
Last planned examination: Autumn 2023
Decision to discontinue this course:
No information inserted
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.
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:
- 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
Recommended prerequisites
Equipment
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
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
Opportunity to raise an approved grade via renewed examination
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.