INF4232 – Logic for System Analysis
The main two goals of this course are:
1. To show how logical methods can be used to model and reason about data types and distributed systems.
2. To give a high-level introduction to distributed systems.
The course therefore briefly introduces different classes of distributed systems -- including transport protocols, database protocols, classic distributed algorithms, and cryptographic protocols -- as well as different forms of communication and some fault tolerance. Modeling and analysis of distributed systems, and an introduction to different classes of requirements of distributed systems. Formalizing requirement specifications, and analyzing whether a system satisfies its requirements.
Equational logic and rewriting logic and the analysis tool Maude are used to formalize and reason about the systems, in addition to reasoning about properties such as termination and invariance.
After having completed this course:
- are you familiar with some classical distributed systems/algorithms
- do you have an understanding of the challenges involved in designing distributed systems
- are you able to model distributed systems, such as distributed algorithms, network protocols and cryptographic protocols, at a high level of abstraction
- are you able to develop and test prototypes/models of such systems
- are you able to reason mathematically about properties of systems, such as correctness and termination
- do you understand different forms of communication and networks
- are you familiar with key classes of requirements that a distributed systems may have to satisfy
- you are able to formalize requirement specifications using temporal logic, and can check whether a system satisfies its requirements
Students admitted at UiO must apply for courses in Studentweb. Students enrolled in other Master's Degree Programmes can, on application, be admitted to the course if this is cleared by their own study programme.
Nordic citizens and applicants residing in the Nordic countries may apply to take this course as a single course student.
If you are not already enrolled as a student at UiO, please see our information about admission requirements and procedures for international applicants.
- 10 credits overlap with INF3232 – Logic for System Analysis
- 9 credits overlap with INF4231 – Formal Modelling and Analysis of Communicating Systems (continued)
- 9 credits overlap with INF4230 – Formal modeling and analysis of communicating systems (discontinued)
- 9 credits overlap with INF3230 – Formal modeling and analysis of communicating systems (continued)
- 9 credits overlap with IN220
- 9 credits overlap with IN220A
- 3 credits overlap with IN307
2 hours of lecture and 2 hours of seminar each week. 3 mandatory assigmnents much be passed during the course. Rules for mandatory assignments.
4 hours written digital exam. The mandatory assignments must be approved prior the exam.
Examination support material
All written and printed exam resources are allowed.
Language of examination
You may write your examination paper in Norwegian, Swedish, Danish or English.
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 will also be counted as one of your three attempts to sit the exam for this course, if you sit the exam for one of the following courses: INF3232/3230/4231/4230.
Special examination arrangements
Application form, deadline and requirements for special examination arrangements.