INF9130 – Selected topics of rewriting logic
Course description
Schedule, syllabus and examination date
Course content
The course is based on INF3230/INF4231 - Formal modeling and analysis of communicating systems and considers fundamental theory for rewriting logic such as Knuth-Bendix completion, reflection, and meta-programming as well as examples of the application of rewriting logic to modeling and analyzing advanced systems in the Maude tool. Examples of such advanced applications may include security and network protocols, real-time systems, mobile systems, and biochemical processes.
Learning outcome
After taking INF9130
- you have a better competence on the formal modeling and analysis of distributed systems at a high level of abstraction, in particular by using the rewriting-logic-based Maude tool
- you know what meta-programming is and you understand the concepts of reflection and metalevel computation in rewriting logic, in particular you can define ad hoc strategies for the execution and analysis of Maude modules by using the meta-programming capabilities of Maude
- you have good knowledge of state-of-the-art applications of rewriting logic to specific domains, such as biochemical processes, real-time computer systems, and mobile processes
- you can specify and analyze system requirements through temporal logic model checking, and in particular by using the Maude linear-time temporal logic model checker
- you know advanced rewriting-logic-based analysis techniques for distributed systems such as narrowing and a custom strategy language
- you have a better insight on how to read and understand scientific papers
- you have some expertise on making scientific presentations.
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
The course builds on INF3230 – Formal modeling and analysis of communicating systems (continued)/INF4231 – Formal Modelling and Analysis of Communicating Systems (continued)/INF220
Overlapping courses
10 credits overlap with INF5130 – Selected topics of rewriting logic (continued)
Teaching
Two - three hours of lectures and group work per week. There will be given mandatory assignments. Rules for mandatory assignments.
Examination
Oral presentation in class (app. 33%). Oral examination at the end of the semester (app. 66%). If many students attend the course, the exam may be written. Mandatory assigmnments must be accepted in order to take the exam.
Grading scale
Grades are awarded on a pass/fail scale. Read more about the grading system.
Explanations and appeals
Resit an examination
Students who can document a valid reason for absence from the regular examination are offered a postponed examination at the beginning of the next semester.
Re-scheduled examinations are not offered to students who withdraw during, or did not pass the original examination.
Withdrawal from an examination
It is possible to take the exam up to 3 times. If you withdraw from the exam after the deadline or during the exam, this will be counted as an examination attempt.
Other
It is strongly recommended to attend the first lecture since it will be given important information.