Seminars

  • Verification of time-sensitive protocols with session types (& friends)

    Laura Bocchi

    University of Kent

    Abstract: 

    In recent work we have extended multiparty session types (MPST) with a model of time borrowed from Communicating Time Automata (CTA). This allowed us to establish a sound and complete correspondence between timed MPST and a subclass of CTA that satisfies progress. On the basis of this correspondence, we can decide properties on CTA that are undecidable in the general case, such as safety (absence of orphan messages and communication mismatches), progress, non-zenoness and eventual reception of messages sent. I will present decidable conditions for these properties, and give a concrete procedure to build *when possible* global timed MPST from (arbitrary) collections of timed automata, with the guarantee that the resulting global specification is a well-behaved composition.

    Where: 
    6.3.5
    When: 
    Thursday, May 25 2017
    Time: 
    15:30
  • Binary session types for psi-calculi

    Hans Hüttel

    Department of Computer Science, Aalborg University, Denmark

    Abstract: 

    Binary session types can be used to describe communication protocols, and to ensure a variety of properties, e.g. deadlock freedom, liveness, or secure information flow. Session type systems are often formulated for variants of the pi-calculus, and for each such system, the central properties such as session fidelity must be re-established.

    The framework of psi--calculi introduced by Bengtson et al. makes it possible to give a general account of variants of the pi-calculus. We use this framework to describe a generic session type system for variants of the pi-calculus. In this generic system, standard properties, including fidelity, hold at the level of the framework and are then guaranteed to hold when the generic system is instantiated.

    We show that our system can capture existing systems including the session type system due to Gay and Hole, a type system for progress due to Vieira and Vasconcelos and a refinement type system due to Baltazar et al. The standard fidelity property is proved at the level of the generic system, and automatically hold when the system is instantiated.

    Where: 
    6.3.38
    When: 
    Friday, September 30 2016
    Time: 
    11:00
  • Static Deadlock Detection for Go by Global Session Graph Synthesis

    Nicholas Ng

    Imperial College London

    Abstract: 

    Go is a programming language developed at Google, with channel-based concurrent features based on CSP. The Go runtime can detect global communication deadlocks when all threads of execution are blocked during execution, but deadlocks in other paths of execution could go undetected.
    In this talk I will present a new static analyser for Go to find potential communication errors such as communication mismatch and deadlocks at compile time. The tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, a recent theoretical result on choreography synthesis is applied to the CFSMs to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors.
    The technique was implemented as a tool, and was applied to analyse common Go concurrency patterns and an open source application with over 700 lines of code.

    Where: 
    6.3.38
    When: 
    Friday, September 16 2016
    Time: 
    11:00
  • A rational reconstruction of homogeneous meta-programming

    Martin Berger

    Department of Informatics, University of Sussex

    Abstract: 

    Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present the first foundational calculus which can model powerful HGMP languages such as Template Haskell. The calculus is designed such that we can gradually enhance it with the features needed to model many of the advanced features of real languages. As a demonstration of the flexibility of our approach, we also provide a simple type system for the calculus. We discuss the difficulties we encountered with formalising HGMP using Nominal Isabelle.

    Where: 
    6.3.5
    When: 
    Tuesday, June 21 2016
    Time: 
    11:00
  • Efficient Model Based Diagnosis with Maximum Satisfiability

    Alexey Ignatiev

    FC, University of Lisbon

    Abstract: 

    Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spreadsheets, web services, and hardware designs, but also the analysis of biological systems, among many others. Motivated by these different uses, there have been significant improvements made to MBD algorithms in recent years. Nevertheless, the analysis of larger and more complex systems motivates further improvements to existing approaches. The talk will briefly describe our recent work on this topic, which proposes a novel encoding of MBD into maximum satisfiability (MaxSAT). The new encoding builds on recent work on using Propositional Satisfiability (SAT) for MBD, but identifies a number of key optimizations that are very effective in practice. Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art.

    Where: 
    6.3.5
    When: 
    Tuesday, May 31 2016
    Time: 
    11:00
  • Network Interdiction problem and Sustainable Networks

    Jean-Francois Baffier

    University of Tokyo

    Abstract: 

    Various kind of networks are used everyday by industrials and academician, but also in everyday life. Whether it be for the road network, water supplies, or telecoms, all share a common goal : sending data or matter between different nodes. Those exchanges can be modeled as flow sent between a source (or sources) and a sink (or sinks). Then a classical approach is to optimize the amount of flow. There is a natural interest in theory and in practice to study the robustness and sustainability of such a flow. The Network Interdiction Problem and its variants can be applied directly to evaluate the efficiency of a flow in case of attacks or failures. Unfortunately, the problem from this family are all NP-hard. In our work, we design a set of exact and approximate algorithms that we evaluate on several kind of networks. The fundamental nature of those algorithms allows us to optimize the cost to establish or of a new network and/or reduce the upkeep of an existing structure while guaranteeing the efficiency of the flows based on the scale of possible attacks. The results on those resilient flows are similar to the classical case, providing a large range of applications.

    Bio: Jean-Francois Baffier graduated Master course at University Paris XI in 2011 and got Ph.D. from the University of Tokyo in 2015. His main research topic covers modeling of failures and routing in Networks. Other research topics involve Game analysis and AI for Games (in particular Starcraft), but also Local Search algorithm (HPC) and limited memory algorithms. He is currently member of the NII (National Institute for Informatics) - JST-ERATO Kawarabayashi Large Graph Project, University of Tokyo.

    Where: 
    6.3.5
    When: 
    Tuesday, January 26 2016
    Time: 
    14:00
  • Certifying Data in Multiparty Session Types

    Bernardo Toninho

    Imperial College London

    Abstract: 

    Multiparty session types are a typing discipline and methodology to
    ensure communication safety in protocols involving two or more
    concurrent participants.

    In this talk I will present the integration of value dependent types
    in a multiparty session typed framework (i.e. types that depend on the
    exchanged data values), enabling static assurances of not only
    communication safety but also of properties of the data itself.
    I will discuss the main tensions, challenges and trade-offs of
    adopting such a framework in the context of multiparty conversations,
    as well as a few simple extensions that increase the flexibility and
    expressiveness of the framework such as so-called “ghost variables” and
    provenance information tracking in a distributed setting.

    I will also elaborate on some potential avenues of future research based
    on this framework.

    Where: 
    6.3.5
    When: 
    Thursday, December 17 2015
    Time: 
    9:30
  • A Data Manipulation Language for Heterogeneous Environments.

    João Costa Seco

    FCT / Universidade Nova de Lisboa

    Abstract: 

    One key aspect of data-centric applications is the manipulation of persistent data repositories, which is moving fast from querying a centralized relational database to the ad-hoc combination of constellations of data sources. Query languages are being typefuly integrated in host, general purpose, languages in order to increase reasoning and optimizing capabilities of interpreters and compilers. However, not much is being done to integrate and orchestrate different and separate sources of data.

    We present a common data manipulation language, that abstracts the nature and localization of the data-sources. We define its semantics and a type directed compilation, query optimization, and query orchestration mechanism to be used in development tools for heterogeneous environments. We provide type safety and language integration. Our approach is also suitable for an interactive query construction environment by rich user interfaces that provide immediate feedback on data manipulation operations. This approach is currently the base for the data layer of a development platform for mobile and web applications.

    (joint work with Paulo Ferreira and Hugo Lourenço, OutSystems SA)

    Where: 
    6.3.38
    When: 
    Wednesday, December 2 2015
    Time: 
    16:00
  • Ownership and Reference Counting based Garbage Collection in the Actor World

    Juliana Franco

    Imperial College London

    Abstract: 

    We propose Pony-ORCA, a fully concurrent protocol for garbage collection in the actor paradigm. It allows actors to perform garbage collection concurrently with any number of other actors. It does not require any form of synchronization across actors except those introduced through the actor paradigm, i.e., message send and message receive.

    Pony-ORCA is based on ideas from ownership and deferred, distributed, weighted reference counting. It adapts the messaging system of actors to keep the reference count consistent.

    We introduce a formal model and describe the invariants on which it relies. We illustrate these invariants through an example and sketch how they are maintained. We show some benchmarks and argue that the protocol can be implemented efficiently.

    Joint work with Sylvan Clebsch, Sebastian Blessing and Sophia Drossopoulou.

    Where: 
    6.3.5
    When: 
    Thursday, July 2 2015
    Time: 
    11:30
  • Erlang multicore applications

    Wojciech Turek

    AGH University of Science and Technology, Krakow, Poland

    Abstract: 

    The development of multi-core architectures is incredibly fast and multicore CPUs can be found nowadays not only
    in supercomputers, but also in ordinary laptops or even phones. Efficient use of multicore architectures requires applying suitable languages and technologies, like Erlang.
    Its concurrency model, based on lightweight processes and asynchronous message-passing, seems very well suited for running massively
    concurrent code on many cores. Most of existing Erlang industrial applications are deployed on computers with up to 24 CPU cores, and
    there are hardly any reports on using Erlang on architectures exceeding 32 cores. We present our experiences with scaling a
    computationally-intensive applications in Erlang up to 64 cores, using as examples global optimization and urban traffic planning problems.

    Where: 
    6.3.5
    When: 
    Thursday, June 4 2015
    Time: 
    11:00

Pages

Subscribe to Seminars