Resiliency problems: algorithms and applications in access control

We present a notion of resiliency for decision problems, which consists in deciding whether an instance of a given problem remains positive after any (appropriately defined) perturbation has been applied to it. In order to tackle these kinds of problems, we introduce a resiliency version of a Integer Linear Program (ILP), and present an algorithm for testing whether an ILP is resilient. As a direct application of our approach, we study a problem arising in the field of access control and establish its parameterized complexity with respect to several parameterizations, establishing the frontier between tractable and intractable cases. This is joint work with Jason Crampton, Gregory Gutin and Martin Koutecky.

Provably Total NP Search Problems of Bounded Arithmetic

Bounded Arithmetic forms a collection of weak theories of Peano Arithmetic related to complexity classes of functions like the Polynomial Time Hierarchy. Many connections between Bounded Arithmetic and important questions about complexity classes have already been established. Recent research considers total NP search problems in the context of Bounded Arithmetic. Total NP search problems have been studied by Papadimitriou et al as a means to characterise the complexity of natural search problems which cannot be analysed as decision problems.

In my talk I will briefly review the research programme of characterising the provably total NP search problems in Bounded Arithmetic, and explain why it is important for current research questions in the area. I will aim to describe a particular result about the provably total NP search problems of Bounded Arithmetic theories related to PSPACE and EXPTIME reasoning.

Partial vertex covers and clusterings of graphs

We will consider the partial vertex cover problem in the class of bipartite graphs. We will also consider a clustering problem on directed acyclic graphs. Our main goal is to address these problems from the perspective of exact and approximate solvability. We will present some new results in these directions.

Logic, Artificial Intelligence and Human Thinking

Symbolic logic has been used in artificial intelligence over the past 60 years or so, in the attempt to program computers to display human levels of intelligence. As a result, new forms of computational logic have been developed, which are both more powerful and more practical. The new computational logic is the logic of an intelligent agent whose mission in life is to make its goals true, by performing actions to change the world, in the context of changes in the world that are outside its control. For this purpose, the agent uses its beliefs in logical form both to reason forwards, synthetically to derive consequences of its observations and candidate actions, and to reason backwards, analytically to reduce goals to subgoals, including actions.

I will argue that computational logic can be used not only for artificial intelligence, but for more conventional computing; and because it improves upon traditional logic, it can also be used for the original purpose of logic, to help people improve their own natural intelligence.

Dynamic social networks and reciprocity: models versus behavioural studies

Many models of social network formation implicitly assume that network properties are static in steady-state. In contrast, actual social networks are highly dynamic: allegiances and collaborations expire and may or may not be renewed at a later date. Moreover, empirical studies show that human social networks are dynamic at the individual level but static at the global level: individuals' degree rankings change considerably over time, whereas network level metrics such as network diameter and clustering coefficient are relatively stable.

There have been some attempts to explain these properties of empirical social networks using agent-based models in which agents play social dilemma games with their immediate neighbours, but can also manipulate their network connections to strategic advantage. However, such models cannot straightforwardly account for reciprocal behaviour based on reputation scores ("indirect reciprocity"), which is known to play an important role in many economic interactions.

In order to account for indirect reciprocity, we model the network in a bottom-up fashion: the network emerges from the low-level interactions between agents. By so doing we are able to simultaneously account for the effect of both direct reciprocity (e.g. "tit-for-tat") as well as indirect reciprocity (helping strangers in order to increase one's reputation).
We test the implications of our model against a longitudinal dataset of Chimpanzee grooming interactions in order to determine which types of reciprocity, if any, best explain the data.

k-means for Streaming and Distributed Big Sparse Data

We provide the first streaming algorithm for computing a provable approximation to the k-means of sparse Big data. Here, sparse Big Data is a set of n vectors in R^d, where each vector has O(1) non-zeroes entries, and d > n. E.g., adjacency matrix of a graph, web-links, social network, document-terms, or image-features matrices. Our streaming algorithm stores at most log(n)*k^{O(1)} input points in memory. If the stream is distributed among M machines, the running time reduces by a factor of M, while communicating a total of Mk^{O(1)} (sparse) input points between the machines.

Guiding program analyzers toward unsafe executions

Most static program analysis techniques do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions, such as the absence of arithmetic overflow. In the first part of the talk, I will present a technique to complement partial verification results by automatic test case generation. In contrast to existing work, our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified, and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions, leading to smaller and more effective test suites.
In the second part of the talk, I will describe a new program simplification technique, called program trimming. Program trimming is a program pre-processing step to remove execution paths while retaining equi-safety (that is, the generated program has a bug if and only if the original program has a bug). Since many program analyzers are sensitive to the number of execution paths, program trimming has the potential to improve their effectiveness. I will show that program trimming has a considerable positive impact on the effectiveness of two program analysis techniques, abstract interpretation and dynamic symbolic execution.

Polynomial Fixed-Parameter Algorithms: A Case Study for Longest Path on Interval Graphs

We study the design of fixed-parameter algorithms for problems already known to be solvable in polynomial time. The main motivation is to get more efficient algorithms for problems with unattractive polynomial running times. Here, we focus on a fundamental graph problem: Longest Path, that is, given an undirected graph, find a maximum-length path in G. Longest Path is NP-hard in general but known to be solvable in O(n^4) time on n-vertex interval graphs. We show how to solve Longest Path on Interval Graphs, parameterized by vertex deletion number k to proper interval graphs, in O(k^{9}n) time. Notably, Longest Path is trivially solvable in linear time on proper interval graphs, and the parameter value k can be approximated up to a factor of 4 in linear time. From a more general perspective, we believe that using parameterized complexity analysis may enable a refined understanding of efficiency aspects for polynomial-time solvable problems similarly to what classical parameterized complexity analysis does for NP-hard problems.

Explaining individual predictions of an arbitrary model

After a brief overview of our research in the field of machine learning and data mining I will present a general method for explaining individual predictions of arbitrary classification and regression models. The method is based on fundamental concepts from coalitional game theory and predictions are explained with contributions of individual feature values. All subsets of input features are perturbed, so interactions and redundancies between features are taken into account. We overcome the method’s initial exponential time complexity with a sampling-based approximation. The method is efficient and its explanations are intuitive and useful. Besides individual predictions, the method can also be used to explain the whole models.

Convention Emergence and Concept Spread in Complex Social Networks

Conventions are often used in multi-agent systems to achieve coordination amongst agents without creating additional system requirements (such as norms or obligations). Encouraging the emergence of robust conventions via fixed strategy agents is an established method of manipulating how conventions emerge. The propagation of conventions is a form of influence spread, and the use of fixed strategy agents for manipulating convention emergence is closely related to the influence maximisation problem in social networks. In this talk we consider (i) using fixed strategy agents to manipulate conventions, (ii) influence maximisation and minimisation in multi-concept networks, and (iii) a methodology for influence estimation.

The Road to Utopia: challenges in linking literature and research data

This presentation describes a personal journey in which a lifetime preoccupation with protein sequences and databases led to the unlikely development of Utopia Documents, a 'smart' PDF reader (http://getutopia.com), and a pioneering project to create the "Semantic Biochemical Journal". Our quest was motivated by a desire to better link data and software tools with scientific articles, to soften the boundaries between databases and papers. During an era of "big data", when more articles are being published and more data are being produced than humans can readily assimilate, Utopia Documents offers a new paradigm for extracting nuggets of information from the barrage of published scientific information that now assaults us every day. Examples will be given from the Lazarus project, in which Utopia harnesses the power of the "crowd" to capture asserted facts and relationships automatically, as a simple side-effect of reading and interacting with scientific articles.

A survey on dynamic graph algorithms and complexity

In this talk I will survey exciting past progresses and future opportunities in developing algorithms and complexity theory for dynamic graph problems. I will discuss barriers and intermediate steps in resolving some of the central graph problems in the area, such as connectivity, minimum spanning tree, shortest paths and maximum matching, I will also discuss how ideas and techniques from other areas – such as spectral method, sketching, algebraic techniques, primal/dual method, and distributed/parallel algorithms -- came into play in developing dynamic graph algorithms.

Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants

Corecursion is a mechanism for defining functions that produce infinite objects such as streams, lazy lists and infinite-depth trees. Establishing corecursion schemes that are expressive, sound and automatic is a notoriously hard problem. I will discuss an approach, implemented in the proof assistant Isabelle/HOL, for "training" a logical system to learn stronger and stronger schemes on a sound basis. The central notion is that of a friendly operator (or friend), which constitutes a safe context for corecursive calls. The framework relies on the ability to recognize friends quasi-automatically by verifying some relational parametricity conditions.

My talk will also include a general discussion about proof assistants and the advantages they have over traditional programming languages.
(joint work with Jasmin Blanchette, Aymeric Bouzy , Andreas Lochbihler and Dmitriy Traytel)

“We have it all wrong”… so what are you doing to change practice?

Along with many other researchers, I share the view that a systematically coherent research program, in both theory and applications of algorithms, is definitely needed to accelerate innovation in computing. We routinely design computational approaches and engage in healthy competitions where the performance of our methods is tested… but what if “We have it all wrong”? What if we need a paradigmatic change in our practice for the development and design of computational methods? We may need to enrich our practice with a new approach.

In fact, John N. Hooker already alerted the computing and mathematical community more than 20 years ago [Hooker, 1995; Journal of Heuristics]: “Competitive testing tells us which algorithm is faster but not why.” Hooker argued for a more scientific approach and he proposed the use of ‘controlled experimentation’. This is common in empirical sciences. “Based on one’s insights into an algorithm”, he said, “one may expect good performance to depend on a certain problem characteristic”. Then “design a controlled experiment that checks how the presence or absence of this characteristic affects performance” and, finally, “build an exploratory mathematical model that captures the insight [...] and deduce from its precise consequences that can be put to the test”. In this talk, I will address how a new thinking is needed for the development of our field. I will have an with emphasis in our success on both speeding up solutions for the traveling salesman problem as well as our success to create very hard instances for the world’s fastest solver.

Provability of weak circuit lower bounds

Proving lower bounds on the size of Boolean circuits computing explicit Boolean functions is a fundamental problem in the theory of computational complexity. In particular, it presents one of the main approaches to the separation of P and NP, and is closely related to the construction of various learning algorithms. Unfortunately, it is also known as a notoriously hard problem. This triggered the investigation of its proof complexity with a well-known discovery of the natural proofs barrier.

A systematic description of proof complexity of circuit lower bounds can be given in terms of mathematical logic. In this framework, one attempts to show that all existing circuit lower bounds are derivable in a constructive mathematical theory while at the same time no such theory is able to prove strong circuit lower bounds separating P and NP. We will describe the state of the art in this area and focus specifically on giving more constructive proofs of known circuit lower bounds including lower bounds for constant-depth circuits and monotone circuits. These proofs take place inside theories of bounded arithmetic formalizing feasible reasoning or, alternatively, in various extensions of Frege propositional proof system.

Towards a reliable prediction of conversion from Mild Cognitive Impairment to Alzheimer’s Disease: a conformal prediction approach using time windows

Predicting progression from a stage of Mild Cognitive Impairment to Alzheimer’s disease is a major pursuit in current dementia research. As a result, many prognostic models have emerged with the goal of supporting clinical decisions. Despite the efforts, the clinical application of such models has been hampered by: 1) the lack of a reliable assessment of the uncertainty of each prediction, and 2) not knowing the time to conversion. It is paramount for clinicians to know how much they can rely on the prediction made for a given patient (conversion or no conversion), and the time windows in case of conversion, in order to timely adjust the treatments. Supervised learning approaches to tackle these issues have been explored. We proposed a Time Windows approach to predict conversion of MCI to dementia, learning with patients stratified using time windows, thus fine-tuning the prognosis regarding the time to conversion. Moreover, to assess class uncertainty, we evaluated the Conformal Prediction approach on the task of making predictions with precise levels of confidence. These confidence measures can provide insight on the likelihood of each prediction.

Explainable Planning for Trustworthy Human-Autonomy Teaming

As AI is increasingly being adopted into application solutions, the challenge of supporting interaction with humans is becoming more apparent. Partly this is to support integrated working styles, in which humans and intelligent systems cooperate in problem-solving, but also it is a necessary step in the process of building trust as humans migrate greater responsibility to such systems. The challenge is to find effective ways to communicate the foundations of AI-driven behaviour, when the algorithms that drive it are far from transparent to humans. In this talk we consider the opportunities that arise in AI planning, exploiting the model-based representations that form a familiar and common basis for communication with users, particularly in scenarios involving human-autonomy teaming.

To iterate or not to iterate: A linear time algorithm for recognizing almost-DAGs

Planarity, bipartiteness, and (directed) acyclicity are basic graph properties with classic linear time recognition algorithms and the problems of testing whether a given graph has k vertices whose deletion makes it planar, bipartite, or (directed) acyclic, are fundamental NP-complete problems when k is part of the input. However, it is known that for any fixed k, there is a linear time algorithm to test whether a graph is k vertex deletions away from being planar or bipartite. On the other hand, it has remained open whether there is a similar linear time recognition algorithm for digraphs which are even only 2 vertex deletions away from being a DAG.

The subject of this talk is a new algorithm that, for every fixed k, runs in linear time and recognizes digraphs which are k vertex deletions away from being acyclic, thus mirroring the case for planarity and bipartiteness. This algorithm is designed via a new methodology that can be used in combination with the technique of iterative compression from the area of Fixed-Parameter Tractability and applies to several ``cut problems’’ on digraphs. This is joint work with Daniel Lokshtanov (University of Bergen, Norway) and Saket Saurabh (The Institute of Mathematical Sciences, India).

COSHER: Compact Self-Healing Routing Algorithms

Compact Routing is a long standing problem of interest in the distributed algorithms community, both in theory and practice. Compact routing looks at reducing the space needed for routing in networks trading it off with length of the paths individual nodes travel. Most solutions for compact routing are static in the sense that the underlying network does not change once the routes have been established. It is challenging to achieve compact routing if the network is dynamic. Self-healing is a paradigm that allows maintenance of network properties, such as the network topology, despite node deletions and insertions, in ‘reconfigurable’ networks such as peer-to-peer and overlay networks. COSHER gives early solutions to achieve compact routing in dynamic networks. This research is now supported by an EPSRC first grant (also titled COSHER) with early results published at ICDCN and Theoretical Computer Science (journal) 2016.

JaVerT: JavaScript Verification Toolchain

The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We will present JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications, of critical JavaScript code. We will describe the JaVerT verification pipeline, focusing on: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language well suited for verification; and JSIL Verify, a semi-automatic verification tool based on a sound program logic for JSIL. We illustrate how JaVerT can be used to specify and verify JavaScript data structure libraries written in object-oriented style using the example of a JavaScript implementation of a key-value map. Finally, we will show how to use standard symbolic execution techniques for debugging JaVerT specifications in order to find concrete witnesses for bugs in both specification and code. Further details can be found in the eponymous paper to be presented at POPL’18.

Research Challenges in a Modern Web Browser

Today, web browsers are just as complex as operating systems. However, I believe there is a shortage of exciting and practical research in this space. In this overview talk, I will cover some recent results and research challenges that pertain to browser security, privacy, and performance. I will talk about some of the issues surrounding a new wave of browser performance wars. I will talk about issue related to user tracking, ad blocking, and anti-ad blocking. Finally, I will talk about some of the challenges of sophisticate browser exploitation that involves data-oriented programming. The talk will focus on both the state of the art and outstanding research challenges.

Retrospective training slow HMM-SCOT emissions model

The Baum-Welsh recurrent ML estimation of HMM parameters has been successfully applied to speech recognition. Its application to Genome modeling is questionable since assigning independence and equal probabilities to emissions from the same part of genome is a rough approximation. We develop a hybrid slow HMM switching model with SCOT emissions which might be a more realistic model for Genome, analysis of combined authorship of literary works, seismological data or financial time series with piecewise volatility. Our combined online and offline segmentation stage estimates time regions with constant HMM states using homogeneity test for SCOT emissions strings. This is made recurrently in parallel on a cluster.