The 7th IFIP WG 1.8 Workshop on Trends in Concurrency Theory

September 8, 2018, Beijing, China

A satellite event of CONCUR 2018

IFIP

   

Description

TRENDS 2018 is an event organised by IFIP WG 1.8 on Concurrency Theory. It aims at bringing together researchers interested in Concurrency Theory and its applications, to exchange ideas and discuss recent trends and open problems. The event will take place on September 8, 2018 and will consist of two invited talks, a number of highlight presentations. It will be associated with the yearly WG 1.8 business meeting.

 

Invited Speakers

  • Nobuko Yoshida, Imperial College, London, UK

    Title: 
    Behavioural Type-Based Static Verification Framework for Go


  • Marielle Stoelinga, University of Twente, The Netherlands

    Title: Risk management for high tech systems
     

Highlight Talks

  • Lei Bu, Path-Oriented Reachability Analysis of Composed Linear Hybrid Systems under Shallow Synchronization Semantics.

  • Zhenbang Chen, Symbolic Verification of MPI Programs.

  • Chen Fu, Andrea Turrini, Xiaowei Huang, Lei Song, Yuan Feng and Lijun Zhang Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems.
  • Cong Tian, Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-Guided Approach.

 

Final Program


    •    09:00-09:15  Arrival and registration

    •    09:15-09:30  Opening


    •    09:30-10:30  Invited Talk:  Nobuko Yoshida, Imperial College, London, UK




 Title:  Behavioural Type-Based Static Verification Framework for Go



Abstract: 

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.
In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

Short talks:  chairs: Javier Esparza and Uwe Nestmann



    •    10:30-11:00  Lei Bu. Path-Oriented Reachability Analysis of Composed Linear Hybrid Systems under Shallow Synchronization Semantics.

    •    11:00-11:30  Coffee / Tea Break

    •    11:30-12:00  Zhenbang Chen. Symbolic Verification of MPI Programs.

    •    12:00-12:30  Chen Fu, Andrea Turrini, Xiaowei Huang, Lei Song, Yuan Feng and Lijun Zhang. Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems.

    •    12:30-13:00  Cong Tian. Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-Guided Approach.

    •    13:00-14:30  Lunch

    •    14:30-15:30  Invited Talk:  Marielle Stoelinga, University of Twente, The Netherlands

         Title: Risk management for high tech systems

        Abstract:


How do we ensure that self-driving cars, nuclear power plants and Internet-of-things devices are safe and reliable? That is the topic of risk management. Fault tree analysis is a very popular technique here, deployed by many institutions like NASA, ESA, Honeywell, Ford, Airbus, the FDA, Toyota, Shell etc.
In this presentation, I will elaborate how the deployment of stochastic model checking can improve the capabilities of fault tree analysis, making them more powerful, flexible and  efficient, allowing one to analyze a richer variety of questions faster, and thereby increasing their practical relevance and deployment in practical risk assessments.
I will report on our experience with the application and validation of these techniques in industrial practice. Finally, I will present some ideas on the deployment of big data analytics within fault tree analysis.



    •    15:30-16:00   Coffee / Tea Break  

    •    16:00-16:30   IFIP WG 1.8 Business Meeting (Open to Public)   

 

Participation

Participation, both to the workshop and to the IFIP WG 1.8 meeting, is open to everybody. For registration, please consult the CONCUR 2018 registration page

 

Organizers

Ilaria Castellani (INRIA Sophia Antipolis, France)

Mohammad Mousavi (University of Leicester, UK)

 

IFIP WG 1.8 on Concurrency Theory

 

The aims of IFIP WG 1.8 on Concurrency Theory are:

 

* To develop theoretical foundations of concurrency, exploring frontiers of existing theoretical models like process algebra and process calculi, so as to obtain a deeper theoretical understanding of concurrent and parallel systems.

* To promote and coordinate the exchange of information on concurrency theory, by sharing ideas, discussing open problems, and identifying future directions of research in the area.

The activities of this WG encompass all aspects of concurrency theory and its applications.

More information on IFIP WG 1.8 can be found on its home page

 

History

 

The first instalment of TRENDS (TRENDS 2012) was held on September 8, 2012 as a satellite event of CONCUR 2012, in Newcastle upon Tyne, UK. 

The second instalment of TRENDS (TRENDS 2013) was held on August 31, 2013 as a satellite event of CONCUR 2013, in Buenos Aires, Argentina.

The third instalment of TRENDS (TRENDS 2014) was held on September 6, 2014 as a satellite event of CONCUR 2014, in Rome, Italy.

The fourth instalment of TRENDS (TRENDS 2015) was held on September 6, 2015 as a satellite event of CONCUR 2015, in Madrid, Spain.

The fifth instalment of TRENDS (TRENDS 2016) was held on August 27, 2016 as a satellite event of CONCUR 2016, in Quebec City, Canada.

The sixth instalment of TRENDS (TRENDS 2017) was held on September 9, 2017 as a satellite event of CONCUR 2017, in Berlin, Germany