INF9130 – Selected topics of rewriting logic

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.


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.

Overlapping courses

10 credits overlap with INF5130 – Selected topics of rewriting logic (continued)


Two - three hours of lectures and group work per week. There will be given mandatory assignments. Rules for mandatory assignments.


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.


It is strongly recommended to attend the first lecture since it will be given important information.

Facts about this course

Autumn 2019
Autumn 2017
Autumn 2015
Autumn 2011

Every other autumn.


Every other Autumn.

Teaching language
Norwegian (English on request)