INF9140 – Specification and verification of parallel systems
Course description
Schedule, syllabus and examination date
Course content
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
Learning outcome
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 candidate 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.
Admission
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.
Prerequisites
Recommended previous knowledge
INF3230 – Formal modeling and analysis of communicating systems (continued)/INF220.
Overlapping courses
10 credits overlap with INF5140 – Specification and verification of parallel systems (continued)
5 credits IN315.
Teaching
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.
Examination
Written or oral exam.
Grading scale
Grades are awarded on a pass/fail scale. Read more about the grading system.
Explanations and appeals
Other
Note that the first lecture is compulsory.