School of Computer Science, IPM

Home

News

Events

Projects

People

Publications

Vacancies

Grant

Scientific Council

Top-Tier Conferences

Home

Invited Lecturers

Organizers

Programme

Registration

Visa

The First IPM Advanced School on Computing:
Formal Methods for Design and Analysis of Computer Systems
11-15 January 2016
Tehran, Iran

Joseph Sifakis, EPFL & Verimag/CNRS [Turing Award winner of 2007]

Title: Model-based system design
Abstract: We will follow the structure of the course "Model-based System Design" presented at EPFL (link: http://risd.epfl.ch/mbsd). The overall aims are:

To understand key issues and methodological aspects in system design
To learn theory and methods for modelling, verifying and designing systems
To outline strengths and limitations of formal methods and learn how they can be effectively applied in system design

The set of topics which will be covered in more or less details also depending on the available time budget, is as following:

Introduction – About Design – Basic Concepts
Transition systems - Basic properties, Operational semantics, Invariants
Petri nets
Process algebras
Timed and Hybrid systems
Temporal Logics
Model Checking – Verification and synthesis techniques
Abstraction techniques – Galois Connections – Abstract Interpretation
Requirements specification languages such as temporal logics and process algebras, and their semantic foundations.
Verification and synthesis techniques and their application for checking/enforcing correctness with respect to given requirements.
Examples of existing model-based design flows and supporting tools

Recommended Literature:

Please follow the link bellow for backgrounds literature:
http://risd.epfl.ch/page-87499-en.html

Wan Fokkink, VU University Amsterdam

Title: The spirit of multicore computing
Abstract: lectures will be based on the following book:
" Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, Morgan Kauffmann, 2008 "
The following parts of the book will be covered:

1.1-1.3, 1.5-1.6: Introduction: SMP and NUMA architectures, flag protocol for mutual exclusion, can protocol for producers-consumers, Amdahl's law
2.1-2.4, 2.8: Mutual Exclusion: Critical sections, locks in Java, Peterson lock, Filter lock, lower bound on the number of locations
3.1-3.2, 3.4-3.8: Concurrent Objects: Pre- and postconditions, linearizability, wait-free bounded queue, sequential consistency, progress properties, volatile variables
5.1-5.4, 5.6-5.8: The Relative Power of Primitive Synchronization Operations: Consensus, impossibility of consensus with atomic registers, 2-thread consensus with a queue, impossibility of 3-thread consensus with a queue, read-modify-write registers, n-thread consensus with compareAndSet
7.1-7.5: Spin Locks: TAS and TTAS locks, exponential back-off, Anderson lock, CLH lock, MCS lock
8.1-8.3: Monitors and Blocking Synchronization: Monitors, conditions, bounded queue with locks and conditions, the lost-wakeup problem, readers-writers lock, synchronized method
10.5-10.6 (not 10.6.1): Concurrent Queues and the ABA Problem: unbounded lock-free queue, ABA problem, Atomic Stamped Reference class
18.1-18.3.7, 18.4: Transactional Memory: What is wrong with locking and compareAndSet, transactions, MESI cache coherence protocol, hardware transactional memory, software transactional memory

Course materials

Slides: http://www.cs.vu.nl/~wanf/ipm2016-slides.pdf
Handouts: http://www.cs.vu.nl/~wanf/ipm2016-handouts.pdf

Recommended Literature:

1- Main reference : The Art of Multiprocessor Programming by Maurice Herlihy and Nir Shavit, Morgan Kauffmann, 2008 "
The main reference can be downloaded from here. Related to each chapter of the main reference, following papers are recommended:
Chapter 3:
2- M. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463–492, 1990
Chapter 5:
3- M. Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems (TOPLAS), 13(1):124–149, 1991
Chapter 7:
4- T. E. Anderson. The performance of spin lock alternatives for shared-memory multiprocessors. IEEE Transactions on Parallel and Distributed Systems, 1(1):6–16, 1990.

5- J. Mellor-Crummey and M. L. Scott. Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Transactions on Computer Systems, 9(1):21–65, 1991
Chapter 8:
6- C. A. R. Hoare. Monitors: an operating system structuring concept. Communications of the ACM, 17(10):549–557, 1974
Chapter 18:
7- M. Herlihy and J. E. B. Moss. Transactional memory: architectural support for lock-free data structures. In Proc. of the Twentieth Annual International Symposium on Computer Architecture, pp. 289–300. ACM Press, 1993

8 - N. Shavit and D. Touitou. Software transactional memory. In Distributed Computing, 10(2):99–116, 1997.

Jan Rutten, Radboud University Nijmegen/CWI

Title: Concrete coalgebra: an introduction by examples
Abstract: Since the early nineties, coalgebra has become an active area of research in which one tries to understand all kinds of infinite data types, automata, transition systems and dynamical systems from a unifying perspective. The focus of coalgebra is on observable behaviour and one uses coinduction as a central methodology, both for behavioural specifications and to prove behavioural equivalences. These days, one uses coalgebraic techniques in a wide variety of areas, ranging from automata theory to software engineering to economy.

In a series of three lectures, we will discuss the following subjects:
(i) The coalgebraic method
(ii) A coinductive calculus of streams
(iii) Algebra meets coalgebra: automata and formal languages

Recommended Literature:

B. Jacobs and J.J.M.M. Rutten. An introduction to (co)algebras and (co)induction
In: Advanced topics in bisimulation and coinduction, pp. 38-99, 2011
J.J.M.M. Rutten. Universal coalgebra: a theory of systems
Theoretical Computer Science 249(1), 2000, pp. 3-80
J.J.M.M. Rutten. A coinductive calculus of streams
Mathematical Structures in Computer Science, Vol. 15, pp. 93-147, 2005
A. Ballester-Bolinches, E. Cosme-Llopez, J. Rutten
The dual equivalence of equations and coequations for automata
CWI Technical Report report FM-1403, 2014, pp. 1--41
F. Bonchi and D. Pous. Hacking nondeterminism with induction and coinduction
Communications of the ACM Vol. 58(2), pp. 87-95, 2015

Slides:

Sung-Shik Jongmans, Open University/Radboud University the Netherlands

Title: Engineering of highly concurrent systems
Abstract: Interaction protocols comprise the most challenging aspect of all types of concurrent software. Traditional models of concurrency are notoriously inadequate for engineering of reliable systems with moderate-to-high levels of concurrency, and by offering the potential for massively concurrent systems, the advent of multicore platforms only exacerbates this inadequacy.
Traditional models of concurrency resort to peculiarly indirect means to express interaction and study its properties. Formalisms such as process algebras/calculi, concurrent objects, actors, agents, shared memory, message passing, etc., all constitute primarily action-based models that provide constructs for the direct specification of things that interact, rather than a direct specification of interaction (protocols). Consequently, interaction in these formalisms becomes a derived or secondary concept whose properties can be studied only indirectly, as the side-effects of the (intended or coincidental) couplings or clashes of the actions whose compositions comprise a model. This inability of traditional models of concurrency to directly treat interaction as a first-class concept lies at the core of the inadequacy of these models for engineering of highly concurrent systems.
Treating interaction as an explicit first-class concept, complete with its own composition operators, gives rise to alternative formal models of concurrency that allow to specify more complex interaction protocols by combining simpler, and eventually primitive, protocols. Reo serves as a premier example of such an interaction based model of concurrency.
In this course, we describe Reo and its support tools. We show how exogenous coordination in Reo reflects an interaction-centric model of concurrency where an interaction (protocol) consists of nothing but a relational constraint on communication actions. In this setting, interaction protocols become explicit, concrete, tangible (software) constructs that can be specified, verified, composed, and reused, independently of the actors that they may engage in disparate applications.

Slides:

Slides are available here.

Elham Kashefi, The University of Edinburgh

Title: Measurement calculus
Abstract: In this series of lecture we present a simple mathematical framework called measurement calculus to explore quantum computation by formalizing a collection of models known as measurement-based quantum computing (MBQC), where the main operation to manipulate information and control computation is measurement. Conceptually MBQC highlights the role of entanglement and separates the quantum and classical aspects of computation; thus it clarifies, in particular, the interplay between classical control and the quantum evolution process. We then present how this model suggests new techniques for designing a new cryptographic quantum protocol, Universal Blind Quantum Computation, which allows a client to have a server carry out a quantum computation for her such that the client's inputs, outputs and computation remain perfectly private, and where she does not require any quantum computational power or memory.

Recommended Literature:

Measurement-based and universal blind quantum computation (More)
Unconditionally verifiable blind computation (More)