INF9140 – Specification and verification of parallel systems
Schedule, syllabus and examination date
Temporal logic for the specification of invariance and liveness properties of parallell systems. Deductive techniques for proving that a parallell system satisfies a temporal logic specification. Automatic verification using model checking techniques
Students will learn how to specify properties of parallell systems using temporal logic and how to verify that such systems satisfy these properties.
In addition, each PhD student will be given an extended curriculum within the field/research area of the course. The syllabus must be approved by the lecturer so that the student can be admitted to the final exam.
PhD candidates from the University of Oslo should apply for classes and register for examinations through Studentweb.
If a course has limited intake capacity, priority will be given to PhD candidates who follow an individual education plan where this particular course is included. Some national researchers’ schools may have specific rules for ranking applicants for courses with limited intake capacity.
PhD candidates who have been admitted to another higher education institution must apply for a position as a visiting student within a given deadline.
Recommended previous knowledge
10 credits overlap with INF5140 – Specification and verification of parallel systems
5 credits IN315.
3 hours of lectures each week. Mandatory problems must be completed during the course; if these are not accepted, the student may not take the final exam.
Written or oral exam.
Grades are awarded on a pass/fail scale. Read more about the grading system.
Explanations and appeals
Note that the first lecture is compulsory.