Current capabilities in computer technology allow enormously complicated implementations of such systems, making the task of producing error-free products more and more difficult. In particular, during the last decade, parallel systems have become a critical part of the infrastructure of our society due to the emergence of modern platforms such as multicores and cloud technology.

It is of great practical and economic importance to developing methods that make the design process less error-prone. There is a real need for techniques for testing and verifying software to guarantee a higher degree of reliability.

Reasoning about concurrent systems is often conducted under the fundamental assumption of sequential consistency (SC) where all components are strongly synchronized so that they all have a uniform view of the global state of the system. However, nowadays, most parallel software run on platforms that do not guarantee SC. More precisely, to satisfy demands on efficiency and energy-saving, such platforms implement optimizations that lead to the relaxation of the inter-component synchronization, hence offering only weak consistency guarantees. Weakly consistent platforms are found at all levels of system design, such as multiprocessors, cache protocols, programming languages, and cloud systems.

The participants will learn:

• The principles of model checking: a technique that has led to the most notable advances in algorithmic program verification during the last 20 years.
• Frameworks for verifying communication protocols, distributed systems and algorithms, timed systems, hardware circuits, concurrent programs, and multicore architectures.
• Modeling and verification through classical models such as timed automata, push-down automata, Petri nets, and lossy channels systems.
• Modeling and verifying concurrent programs running on weakly consistent platforms, such as x86-TSO, IBM Power, ARM, C11, and the cloud.

• Model checking.
• Infinite-state models.
• Reachability analysis.
• Petri nets.
• Timed automata.
• Push-down automata.
• Lossy channel systems.
• x86-TSO.
• C11.
• Well quasi-ordered systems.
• Program abstraction: monotonic abstraction, view abstraction.
• The Power and ARM architectures.
• Parameterized systems.
• Cloud platforms.

• 15 Lectures.
• Project work. The project will consist of implementing some of the algorithms discussed in the class.

• Weekly assignments.
• Project work.

• Course suitable both for PhD and MSc students.
• Primary knowledge corresponding to three years of an undergraduate program in computer science. However, I do not assume any prior knowledge of formal methods, program verification, or weak memory models.

• Intorduction. pdf. keynote.
• Petri Nets. pdf. keynote.
• Well-Quasi-Orderings. pdf. keynote. Summary in keynote.
• Lossy Channel Systems. pdf. keynote.
• x86-TSO. pdf. keynote. Short version in keynote.
• TSO: The Load-Buffer Semantics. pdf. keynote.
• Timed Petri Nets. pdf. keynote.
• Stateless Model Checking -- The C11 Release-Acquire Semantics. pdf. keynote. A short version.
• Timed Petri Nets. pdf. keynote. Part 1 in pdf. Part 1 in keynote. Part 2 in pdf. Part 2 in keynote. Summary.
• View Abstraction. pdf. keynote.

• Lecture 1.
• Lecture 2.1, and Lecture 2.2.
• Lecture 3.
• Lecture 4.
• Lecture 5.
• Lecture 6.
• Lecture 7.
• Lecture 8.
• Lecture 9.
• Lecture 10.
• Lecture 11.
• Lecture 12.
• Lecture 13.
• Lecture 14.
• Lecture 15.

• Parosh Aziz Abdulla. Well- and Better-Quasi-Ordered Transition Systems.

• Parosh Aziz Abdulla.