Invited talks

This year the invited talks at DISC 2016 are:

• Keynote talk by Serge Abiteboul (Senior researcher at INRIA, Professor ENS Cachan)

Serge Abiteboul has been a researcher at the Institut National de Recherche en Informatique et Automatique since 1982 and is now Distinguished Affiliated Professor at Ecole Normale Supérieure de Cachan. He was a Lecturer at the École Polytechnique. He has been Chair Professor at Collège de France in 2011-12 and Francqui Chair Professor at Namur University in 2012-2013. He co-founded the company Xyleme in 2000. Serge Abiteboul has received the ACM SIGMOD Innovation Award in 1998, the EADS Award from the French Academy of sciences in 2007; the Milner Award from the Royal Society in 2013; and a European Research Council Fellowship (2008-2013). He became a member of the French Academy of Sciences in 2008, and a member the Academy of Europe in 2011. His research work focuses mainly on data, information and knowledge management, particularly on the Web.

Personal information management systems and knowledge integration

Personal data is constantly collected, either voluntarily by users in emails, social media interactions, multimedia objects, calendar items, contacts, etc., or passively by various applications such as GPS of mobile devices, transactions, quantified self sensors, etc. The processing of personal data is complicated by the fact that such data is typically stored in silos with different terminologies/ontologies, formats and access protocoles. Users are more and more loosing control over their data; they are sometimes not even aware of the data collected about them and how it is used.

We discuss the new concept of Personal Information Management Systems (PIMS for short) that allows each user to be in a position to manage his/her personal information. Some applications are run directly by the PIMS, so are under direct control of the user. Others are in separate systems, that are willing to share with the PIMS the data they collect about that particular user. In that later case, the PIMS is a system for distributed data management. We argue that the time has come for PIMS even though the approach requires a sharp turn from previous models based on the monetisation of personal data. We consider research issues raised by PIMS, either new or that acquire a new flavor in a PIMS context.

We also present works on the integration of user’s data from different sources (such as email messages, calendar, contacts, and location history) into a PIMS. The PIMS we consider is a Knowledge Base System based on Semantic Web standards, notably RDF and schema.org. Some of the knowledge is “episodical” (typically related to spatio-temporal events) and some is “semantic” (knowledge that holds irrelative to any such event). Of particular interest is the cross enrichment of these two kinds of knowledge based on the alignment of concepts, e.g., enrichment between a calendar and a geographical map using the location history. The goal is to enable users via the PIMS to query and perform analytics over their personal information within and across different dimensions.

• Keynote talk by Graham Cormode (Professor at University of Warwick)

Graham Cormode is a Professor in Computer Science at the University of Warwick. He works on research topics in data management, privacy and big data analysis. Previously, he was a principal member of technical staff at AT&T Labs-Research in the USA. His work has appeared in over 90 conference papers, and 30 journal papers. He has also edited two books on applications of algorithms to different areas, and co-authored a third. He currently serves as an associate editor for ACM Transactions on Database Systems (TODS), and the Journal of Discrete Algorithms.

Matching and Covering in Streaming Graphs

Problems related to (maximum) matchings and vertex covering in graph have a long history in Combinatorics and Computer Science. They arise in many contexts, from choosing which advertisements to display to online users, to characterizing properties of chemical compounds. Stable matchings have a suite of applications, from assigning students to universities, to arranging organ donations. These have been addressed in a variety of different computation models, from the traditional RAM model, to more recent sublinear (property testing) and external memory (MapReduce) models. Matching has also been studied for a number of classes of input graph: including general graphs, bipartite graphs, weighted graphs, and those with some sparsity structure.

We focus on the streaming case, where each edge is seen once only, and we are restricted to space sublinear in the size of the graph (ie., no. of its vertices). In this case, the objective is to find (approximately) the size of the matching. Even here, results for general graphs are either weak or make assumptions about the input or the stream order. In this talk, we describe work which seeks to improve the guarantees in various ways. First, we consider the case when we are given a promise on the size of the solution: the matching is of size at most $k$, say. This puts us in the realm of parameterized algorithms and kernelization, but with a streaming twist. We show that algorithms to find a maximal matching can have space which grows quadratically with $k$. Second, we consider restricting to graphs that have some measure of sparsity — bounded arboricity, or bounded degree. This aligns with reality, where most massive graphs have asymptotically fewer than $O(n^2)$ edges. In this case, we show algorithms whose space cost is polylogarithmic in the size of the input, multiplied by a constant that depends on the level of sparsity, in order to estimate the size of the maximum matching. The techniques used rely on ideas of sampling and sketching, developed to handle data which arrives as a stream of observations, coupled with analysis of the resulting randomized algorithms.

• Keynote talk by Javier Esparza (Professor at Technische Universität München)

Javier Esparza holds the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technische Universität München since 2007. Previously he held the Chair of Software Reliability and Security at the University of Stuttgart (2003-2007), the Chair of Theoretical Computer Science at the University of Edinburgh (2001-2003), and worked as Associate Professor at the Technische Universität München (1994-2001). He has co-authored a book on Free Choice Petri nets with Jörg Desel, and a book on the unfolding approach to Model Checking with Keijo Heljanko. He has published over 150 scientific papers in the fields of automatic program verification, program analysis, concurrency theory, and automata theory. Javier Esparza has contributed to the theory Petri nets, and was one of the initiators of the unfolding approach to model checking, the automata-theoretic approach to software model checking, and the verification of infinite-state systems. More recently he has conducted research on the fundamentals of program analysis and the verification of parametrized and stochastic systems. His group has developed several verification tools, including Moped and jMoped and Rabinizer. Javier Esparza received a honorary doctorate in Informatics from the Masaryk University of Brno in 2009 and is member of Academia Europaea since 2011.

Verification of population protocols

Population protocols (Angluin et al., PODC 2004) are a formal model of sensor networks consisting of identical mobile devices. When two devices come into the range of each other, they interact and change their states. Computations are infinite sequences of pairwise interactions where the interacting processes are picked by a fair scheduler.

A population protocol is well specified if for every initial configuration C of devices and for every fair computation starting at C, all devices eventually agree on a consensus value that only depends on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. The main two verification problems for population protocols are: Is a given protocol well-specified? Does a given protocol compute a given predicate?

While the class of predicates computable by population protocols was already established in 2007 (Angluin et al., Distributed Computing), the decidability of the verification problems remained open until 2015, when my colleagues and I finally managed to prove it (Esparza et al., CONCUR 2015, improved version to appear in Acta Informatica). In the talk I report on our results and discuss some new developments.