The course introduces theory, methods, and tools that are prerequisites for research in the areas of programming languages and formal methods at the division of theoretical computer science.
Information for research students about course offerings
The course is given first time VT2020, and will be repeated every other year, dependent on the intake of PhD students.
Content and learning outcomes
Basic program verification techniques (symbolic execution, abstract interpretation, VC generation, type systems); program logics; inter/intraprocedural flow analysis; Concurrency models, concurrency semantics and verification techniques; Systems modelling and refinement; Modelling, specification, and verification of security properties.
Intended learning outcomes
At the end of the course the student should be able to
- Apply several theories and methods covered in the course on sample problems of limited scope and size
- Evaluate the suitability of a given theory/method within a given problem domain
- Define and execute a first own research project within the students research area
- Account for choice of approach
- Relate own work to the state of the art in the area
The course consists of a number, minimum 4, of modules given by members of faculty and postdocs over a full term = two periods. Each module consists of 3-6 lectures with homework. At the end of the course a take-home exam is given over two days consisting of one problem set per module. Each problem set defines a minimum required pass level. To pass the course at least four problem sets must be completed at pass level. This allows students to focus their attention of a selection of course modules appropriate for their research topic.
Literature and preparations
Mathematical maturity and computer science background commensurate with a masters exam in computer science, electrical engineering, math/physics, or similar masters level education.
Selected surveys, papers, slides, course notes, as suitable for each module.
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
- EXA1 - Examination, 10.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.
The examination is done through the take-home exam as detailed above.
Other requirements for final grade
Passed take-home exam.
Opportunity to complete the requirements via supplementary examination
Opportunity to raise an approved grade via renewed examination
- 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 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 FDD3024