1st MEALS Workshop - Abstracts
Invited speaker
|
Dino Distefano (Queen Mary, University of London, UK) Title: A Voyage to the Deep-Heap |
|
Abstract: This talk is the diary of a journey that brought the theoretical advances of Separation Logic all the way to a commercial static analyzer. It reports on some of the key insights which made this journey possible. It reviews the difficulties we have encountered along the way, the present status, and some of the challenges that remain open. I have shared this journey with Cristiano Calcagno, Peter O’Hearn, and Hongseok Yang. |
Workshop speakers
|
Christel Baier (Technische Universität Dresden, DE) Title: Quantitative analysis of low-level operating system primitives using probabilistic model checking |
| Abstract: |
|
Nicolás Bordenabe (INRIA, FR) Title: Geo-Indistinguishability: Differential Privacy for Location-Based Systems |
| Abstract: The growing popularity of location-based systems, allowing unknown/untrusted servers to easily collect and process huge amounts of users' information regarding their location, has recently started raising serious concerns about the privacy of this kind of sensitive information. We study geo-indistinguishability, a formal notion of privacy for location-based systems that protects the exact location of a user, while still allowing approximate information - typically needed to obtain a certain desired service - to be released. Our privacy definition formalizes the intuitive notion of protecting the user's location within a radius r with a level of privacy that depends on r. We present three equivalent characterizations of this notion, one of which corresponds to a generalized version of the well-known concept of differential privacy. Furthermore, we present a perturbation technique for achieving geo-indistinguishability by adding controlled random noise to the user's location, drawn from a planar Laplace distribution. We demonstrate the applicability of our technique through two case studies: First, we show how to enhance applications for location-based services with privacy guarantees by implementing our technique on the client side of the application. Second, we show how to apply our technique to sanitize location-based sensible information collected by the US Census Bureau. |
|
Jan Friso Groote (Eindhoven University of Technology, NL) Title: Axiomatisation of timed branching bisimulation with unbounded choice |
| Abstract: We present two relatively simple axioms for branching bisimulation in continuous real time process algebra with unbounded summation, conditions and data. In 1990 a natural real time semantics was proposed by Jan Bergstra. Steven Klusener proposed complete axiomatisations for strong and branching bisimulation in the early '90-ies in the context of prefix integration, but the complexity of the axioms in particular and the field in general, led to very little progress during the two decades that followed. Using the framework set up by Bas Luttik to prove completeness for process algebras with unbounded summation and data, we managed to find the axioms characterising continous real time, data, unbounded and even uncountable behavioural choices and conditions. |
|
Joost-Pieter Katoen (RWTH Aachen University, DE) Title: Probabilistic Programs: New Semantic Insights and Loop Analysis Techniques |
| Abstract: We present a connection between McIver and Morgan's wp-semantics of probabilistic programs and a simple operational semantics in terms of parameterized Markov decision processes, and discuss an approach to synthesize loop invariants for such programs. |
|
Axel Legay (INRIA, FR) Title: PLASMA-lab: a flexible, distributable statistical model checking library |
|
Abstract: We present PLASMA-lab, a library that provides the functionality to create custom statistical model checkers based on arbitrary modelling languages -- users need only implement a few simple methods in a simulator class. PLASMA-lab is written in Java for maximum cross-platform compatibility and has already been incorporated in various performance-critical software and embedded hardware platforms. We have constructed a graphical user interface (GUI) that exposes the functionality of PLASMA-lab and facilitates its use as a standalone application with multiple modelling languages. The GUI adds the notion of projects and experiments, and implements a simple, practical means of distributing simulations using remote clients. |
|
Hernán Melgratti (Universidad de Buenos Aires, AR) Title: Realisation of Choreographies and Multi-party Session Types |
| Abstract: Complete realisation of choreographies has been largely neglected in the context of multiparty session types, in which realisation is generally understood as partial. We introduce the notion of whole-spectrum realisation according to which the deterministic implementation of a role of a choreography cannot persistently avoid the execution of a branch of an internal choice specified by that choreography. Although whole-spectrum realisation is defined as a relation between the execution traces of a global type and those of its candidate implementations, it can be checked by using multiparty session types. We represent choreographies as minor variants of the global types of Carbone, Honda, and Yoshida and use local types projections to validate processes in a type system that guarantees whole-spectrum realisability. |
|
Nir Piterman (University of Leicester, UK) Title: The Modal Transition System Control Problem |
| Abstract: |
|
Daniel Sykes (Imperial college, UK) Title: Learning Revised Models For Planning In Adaptive Systems |
| Abstract: Environment domain models are a key part of the information used by adaptive systems to determine their behaviour. These models can be incomplete or inaccurate. In addition, since adaptive systems generally operate in environments which are subject to change, these models are often also out of date. To update and correct these models, the system should observe how the environment responds to its actions, and compare these responses to those predicted by the model. We use a probabilistic rule learning approach, NoMPRoL, to update models using feedback from the running system in the form of execution traces. NoMPRoL is a technique for non-monotonic probabilistic rule learning based on a transformation of an inductive logic programming task into an equivalent abductive one. In essence, it exploits consistent observations by finding general rules which explain observations in terms of the conditions under which they occur. The updated models are then used to generate new plans with a greater chance of success in the actual environment encountered. |
|
Andrea Turrini (Saarland University, DE) Title: The Algorithmics of Probabilistic Automata Weak Bisimulation |
| Abstract: Probabilistic automata are a powerful model for studying properties of concurrent randomized systems. Weak bisimulation allows us to study such qualities in smaller but equivalent automata, thus improving the range of the automata and properties we can study. In this talk we consider the efficiency of deciding weak bisimulation in theory and practice, how we can construct the minimal equivalent automaton, and some extensions. |
|
Anton Wijs (Eindhoven University of Technology, NL) Title: Using General Purpose Graphics Processors for Probabilistic Model Checking |
| Abstract: General Purpose Graphics Processing Units (GPGPUs) are used more and more to perform scientific computing. They offer the potential of many-core parallelisation, which can result in drastic runtime improvements. In this talk, I will explain how GPGPUs can be employed to speed up probabilistic model checking. I will talk about the architecture of NVIDIA GPGPUs, and show how the CUDA programming language can be used to write instructions for them. The particular architectural characteristics of GPGPUs should be taken into account when writing parallel algorithms, and I will explain how a straightforward approach for probabilistic model checking can be further improved. |
