The STRL organises a series of seminars which are held most weeks of the University academic semesters. These are given by members of the laboratory as well as some external speakers.

The list of the forthcoming seminars is given below.

March 2012:

• Dr Nobuko Yoshida, Imperial College London

  Multiparty Session Types and their applications

  Date: Friday 9th March
  Location: Bede Island 0.12
  Time: 13:00--14:00
  

  Abstract

  I talk about an extension of the session types to multiparty, asynchronous interactions, which often arise in practical communication-centred applications. The theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. A global type plays the role of "a shared agreement" among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety and session fidelity are established for general n-party asynchronous interactions.

  I also talk about a summary of recent collaborations, based on multiparty session types, with industry partners and a major, long-term, NSF-funded program which provides a large scale cyberinfrustracture for 25-30 years of sustained ocean measurements to study climate variability, ocean circulation and ecosystem dynamics.

  Back

• Dr Gerhard Schellhorn, University of Augsburg, Germany

  Correctness of Concurrent Lock-Free Algorithms

  Date: Thursday 1st March
  Location: Bede Island 0.12
  Time: 13:00--14:00
  

  Abstract

  With multi-core processors becoming standard in todays computers, research on efficient concurrent algorithms has gained on importance over the last years.

  Efficient implementations of data structures are no longer based on global locks, but either use fine-grained locking or dispose with locking completely, using lock-free synchronisation primitives such as CAS (compare-and-swap). The talk will give an introduction to such algorithms and the problems they must cope with.

  For lock-free algorithms, a uniform argument about the use of locks is no longer sufficient to reduce correctness to standard verification of sequential programs. Instead, individual arguments for the algorithms become necessary to argue that an algorithm is correct.

  The talk will give the main correctness criterion of linearisability, and discuss some proof techniques based on the rely-guarantee (RG) principle that can be used to show correctness of such algorithms. The proof principles have been mechanised in the theorem prover KIV on the basis of interval temporal logic (ITL) and RG to verify interesting lock-free algorithms.

  Back

February 2012:

• Dr Kevin Jones, EADS Innovation Works UK, Homeland Security and CNI Protection

  Protecting the Critical National Infrastructure from Cyber Attack: The Research Questions?

  Date: Friday 24th January
  Location: Bede Island 0.12
  Time: 14:00--15:00
  

  Abstract

  Securing the Critical National Infrastructure (CNI) from Cyber Attacks is the focus of significant global research amongst a background of increased attack vectors and growing interest from governments worldwide. This talk provides an introduction to the Supervisory Control And Data Acquisition (SCADA) systems that form the basis for CNI, and discuss the background and requirements for current research within the area of CNI Cyber Security. The aim is to foster discussion and opportunities through; the use of real-world examples, an overview of the SCADA cyber security problem space, and current research directions including ongoing activities within EADS Innovation Works UK.

  After the talk there will also be an opportunity to discuss current industrial placements at EADS-IW, as well as the potential of MSc projects in collaboration with them.

  Back

January 2012:

• Dr Nobuko Yoshida, Imperial College London

  Multiparty Session Types and their applications

  Date: Thursday 26th January Postponed
  Location: Bede Island 0.12
  Time: 13:00--14:00
  

  Abstract

  I talk about an extension of the session types to multiparty, asynchronous interactions, which often arise in practical communication-centred applications. The theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. A global type plays the role of "a shared agreement" among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety and session fidelity are established for general n-party asynchronous interactions.

  I also talk about a summary of recent collaborations, based on multiparty session types, with industry partners and a major, long-term, NSF-funded program which provides a large scale cyberinfrustracture for 25-30 years of sustained ocean measurements to study climate variability, ocean circulation and ecosystem dynamics.

  Back