INF5130 – Selected topics of rewriting logic

Schedule, syllabus and examination date

Choose semester

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 INF5130

  • 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.


Students who are admitted to study programmes at UiO must each semester register which courses and exams they wish to sign up for in Studentweb.

If you are not already enrolled as a student at UiO, please see our information about admission requirements and procedures.


Recommended previous knowledge

The course builds on INF3230 – Formal modeling and analysis of communicating systems (continued)/INF220

Overlapping courses

10 credits overlap with INF9130 – 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 scale from A to F, where A is the best grade and F is a fail. 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 2011

Autumn 2009

Autumn 2007

Autumn 2006

Autumn 2005

Autumn 2004

Every other autumn.


Every other Autumn.

Teaching language