Overview of Concurrent Programming. The interleaving model. Correctness: Properties of Safety, Liveness, Fairness. Languages: Java and Promela. The issue of Critical Section. Formal methods of verification: iductive proofs and LTL logic. Advanced algorithms for the C.S. problem. Semaphores and their implementation. The problem of the Dining Philosophers. The concept of Monitor. The problem of readers-writers. Communication via channels. Introduction to model checking.
2) Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
Learning Objectives
This course aims at providing students with the basic principles of programming, specification and verification of concurrent systems. This goal is pursued by the introduction of a reference model, in some fundamental synchronization algorithms are described and their correctness is analyzed.
Prerequisites
Familiarity with the basics of sequential programming, a few elements of propositional logic.
Teaching Methods
Lectures in class.
Further information
Office hours: by appointment.
Type of Assessment
Written examination. Discussion of the written examination.
Course program
Overview of Concurrent Programming. The interleaving model. Correctness: Properties of Safety, Liveness, Fairness. Languages: Java and Promela. The issue of Critical Section. Formal methods of verification: iductive proofs and LTL logic. Advanced algorithms for the C.S. problem. Semaphores and their implementation. The problem of the Dining Philosophers. The concept of Monitor. The problem of readers-writers. Communication via channels. Introduction to model checking.