INF5130 – 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 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.
Admission
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.
Prerequisites
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)
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 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.
Other
It is strongly recommended to attend the first lecture since it will be given important information.