Verification of Concurrent Systems Summer School

Aim & Focus Areas

Concurrency is an ever-increasing trend in designing and implementing computer systems. However, their analysis is notoriously challenging due to the combinatorial explosion of their state-spaces. Ad-hoc and manual techniques come short of making any substantial claim regarding quality and correctness of such systems. This school addresses this challenge by presenting a rigorous and expressive modeling framework for specifying such systems and an arsenal of verification techniques to efficiently verify their correctness. We report on several case studies where these techniques have been effectively applied and how they have affected the quality of concurrent and communicating system designs.

Target Audience

The course is intended for graduate students in Computer Science and Engineering and related fields. The course does not assume much prior knowledge apart from some basic affinity with logic and discrete mathematics.

Organizers:

Dates: August 8-10, 2017

Venue: The Verification of Concurrent Systems Summer School will be held at Khatam University located at Hakim Azam Street in Vanak.

Check the photo gallery here

Professor Jan Friso Groote – Eindhoven University of Technology

Jan Friso Groote head of the Formal System Analysis group at Eindhoven University of Technology. He also works one day a week at ASML, the world leading wafer scanner manufacturer. Professor Groote studied computer science at Twente University (The Netherlands).  He received his PhD. degree (with prof.dr. Bergstra as his advisor) from the University of Amsterdam on a thesis entitled `Process Algebra and Structured Operational Semantics’. Subsequently, his research shifted towards practical usability of the theory. To this end, he developed mCRL2, a language and toolset that combines process algebra with data, time, probabilities, modal logics and visualisation. This language and toolset has been used to model, analyse and design a range of systems, including medical protocols, railway control systems, control of storage facilities and software for wafer scanners and the CERN’s particle accelerator in Geneva.

Professor Jan Friso Groote

I very much like Iran and the hospitality of its inhabitants, and enjoyed giving this summer school on verification of concurrent systems equally well.

Professor MohammadReza Mousavi – University of Leicester, UK 

Mohammad Reza Mousavi is a professor of Data-Oriented Software Engineering at University of Leicester, UK and part-time (guest) professor at Gothenburg University and Halmstad University, Sweden. He received his Bachelor and Masters degree from Sharif University of Technology, Iran and
his Ph.D. in Computer Science in 2005 from TU Eindhoven, The Netherlands.  Since then, he has been postdoctoral researcher (2006-2007) at Reykjavik University, Iceland, and  assistant and associate professor (2005-2013) at TU Eindhoven and professor at Halmstad University.
His research interests are in formal semantics and verification and his main current research area in model-based testing, particularly applied to software product lines and cyber-physical systems.

Dr. Hossein Hojjat – Rochester Institute of Technology

Hossein Hojjat is an assistant professor in the Computer Science department at the Rochester Institute of Technology (RIT). Before joining RIT, he was a postdoctoral researcher at Cornell University. He earned a PhD in Computer Science from EPFL in 2013. His research interests center on program synthesis and verification.

Tentative Program

Tuesday (July 8) 
09:00-09:30 Opening, introducing the program, the speakers, and the toolset
09:30-10:15 Introduction lecture: subject matter, possible application areas, success stories (Mohammad Mousavi)
10:15-10:45 Coffee / tea break
10:45-11:15 Actions and processes (Jan Friso Groote)
11:15-11:30 Leg stretcher
11:15-12:00 Behavioural equivalences – Part I  (Mohammad Mousavi)
12:00-13:30 Lunch Break
13:30-14:15 Hands-on session: specification, state-space generation, state-space reduction and visualisation of a toy example (Jan Friso Groote)
14:15-14:45 Coffee / tea break
14:45-15:30 Behavioural equivalences – Part II  (Mohammad Mousavi)
15:30-15:45 Leg stretcher
15:45-16:30 Hands on session: specification of basic requirements and defining interfaces for the case study (Jan Friso Groote)
16:30 – 17:00 Q&A Session
Wednesday  (July 9) 
09:30-09:45 Case Study: Linear Processes
09:45-10:15 Parallel processes (Mohammad Mousavi)
10:15-10:45 Coffee / tea break
10:45-11:15 Abstract data types (Jan Friso Groote)
11:15-12:30 Hennessy Milner Logic  (Mohammad Mousavi)
12:30-13:45 Lunch Break
13:45-14:30 Hands-on session: abstract data types for the case study
14:30 – 18:00 Social event
Thursday (July 10) 
09:30-10:15 Modal mu-Calculus (Mohammad Mousavi)
10:15-11:00 Reasoning about Processes (Jan Friso Groote)
11:00-11:30 Coffee / tea break
11:30-12:15 Hands-on session: specifying the requirements of the case study in logic
12:15-13:30 Lunch Break
13:30-14:15 Hands-on session: Specifying the behavior of the case study
14:15-14:45 Coffee / tea break
14:45-15:30 Hands-on session: verification
15:30-15:45 Leg stretcher
15:45-16:30 Hands on session: verification cont’d
16:30 – 17:00 Q&A Session

Preparation

The summer school includes several hands-on sessions and to benefit from those, you need to prepare a few things before attending the workshop.

  • Please bring along a laptop with you.
  • Please download the mCRL2 toolset from www.mcrl2.org and install it on your laptop by following the instructions given on the above-mentioned website.
  • We will work on with a case study throughout the workshop. However, it is often more instructive if you bring in your own case study: an informal description of a system that you would like to design and verify. You may send us (m.r.mousavi@hh.se, jfg@win.tue.nl) its informal description of your case study (1 a4 page description suffices) before August 5 so that we can familiarise ourselves with your case study and can better help you out during the school.
  • The courses assume no pre-knowledge; however, to benefit most from the school, you may watch the videos from the following MOOCs:
    https://www.coursera.org/learn/automata-system-validation#
    https://learn.canvas.net/courses/1130

Please feel free to send us your questions (m.r.mousavi@hh.se, jfg@win.tue.nl), should you have any.