University of Leicester


Computer Science Seminars

Useful links:

Semester 2, 2016/17

Seminar programme

Seminar details

Computing continuous-time Markov chains as transformers of unbounded observables

Tobias Heindl (University of Leipzig)
Thu, 18 May, 10:00 in ATT 204 (Host: Reiko Heckel)

The talk describes continuous-time Markov chains (CTMCs) as transformers of real-valued functions on their state space, considered as generalised predicates and called observables. Markov chains are assumed to take values in a countable state space S; observables f: S -> ℝ may be unbounded. The interpretation of CTMCs as transformers of observables is via their transition function P: each observable f is mapped to the observable Pf that, in turn, maps each state x to the mean value of f at time t conditioned on being in state x at time 0.

The main result is computability of the time evolution of observables, i.e., maps of the form (t,f) to Pf, under conditions that imply existence of a Banach sequence space of observables on which the transition function P of a fixed CTMC induces a family of bounded linear operators that vary continuously in time (w.r.t. the usual topology on bounded operators). The result is flexible enough to accommodate unbounded observables; explicit examples feature the token counts in stochastic Petri nets and sub-string occurrences of stochastic string rewriting systems. The result provides a functional analytic alternative to Monte Carlo simulation as test bed for mean-field approximations, moment closure, and similar techniques that are fast, but lack absolute error guarantees.

Gradual Session Types

Peter Thiemann (Universitaet Freiburg)
12th May, 14:00 in MSB LT2 (Maurice Shock Building) (Host: Emilio Tuosto)

Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing.

We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.

Authors: A. Igarashi, P. Thiemann, V. Vasconcelos, P. Wadler

Learning via Logic

Clemens Kupke (Strathclyde)
5th May, 14:00 in MSB LT2 (Maurice Shock Building) (Host: Alexander Kurz)

A key result in computational learning theory is Dana Angluin’s L* algorithm that describes how to learn a deterministic finite automaton (DFA) using membership and equivalence queries. In my talk I will present a generalisation of this algorithm using basic ideas from coalgebra and modal logic.

In the first part of my talk I will recall how the L* algorithm works and establish a new connection to modal logic. After that I will use this link to devise an algorithm that covers (known variants of) the L* algorithm and similar algorithms for learning Mealy and Moore machines. Other examples of structures that can be learned by our algorithm are regular infinite streams, regular trees and finite bisimulation quotients of various types of transition systems.

Joint work with Simone Barlocco.

Self-esteem and Social Networks of Neural Networks

Alexander Gorban (talk postponed) (Department of Mathematics, Leicester)
24th March, 14:00 in MSB LT2 (Maurice Shock Building) (Host: Alexander Kurz)

Knowledge Transfer Between AI Systems

Ivan Tyukin (Department of Mathematics, Leicester)
March 17, 14:00 in (Host: Alexander Kurz)

(slides). We consider the fundamental question: how a legacy "student" Artificial Intelligent (AI) system could learn from a legacy "teacher" AI system or a human expert without complete re-training and, most importantly, without requiring significant computational resources. Here "learning" is understood as an ability of one system to mimic responses of the other and vice-versa. We call such learning as Artificial Intelligence knowledge transfer. We show that if a) internal variables of the "student" Artificial Intelligent system have the structure of an n-dimensional topological vector space, b) pre-existing knowledge is more or less evenly represented in a bounded domain of this space, and c) n is sufficiently high then, with probability close to one, the required knowledge transfer can be implemented by simple cascades of linear functionals. In particular, for n sufficiently large, with probability close to one, the "student" system can successfully and non-iteratively learn k<n/2 new examples from the "teacher" (or correct the same number of mistakes) at the cost of two additional inner products. The concept is illustrated with examples of 1) knowledge transfer from a human expert to a pre-trained convolutional neural network and 2) from a pre-trained convolutional neural network to a simple linear HOG-SVM classifier.

A meta-theory of program semantics

Fredrik Dahlqvist (University College London)
Fri, 3rd March, 14:00 in MSB LT2 (Maurice Shock Building) (Host: Alexander Kurz)

Abstract: Program semantics is the art of assigning mathematical meaning to programs, in order to reason formally about them. It is an art because most semantics are tailor made to particular languages and particular problems, for example termination, catching memory bugs, etc. I will sketch some recent work which intends to lay the foundations of a general and principled theory of program semantics. The basic setup is simple: programs can reasonably be expected to be sequentially composable, and their semantics are typically given by some kind of transition systems over a set of possible configurations, for example memory states. In order to include as many types of computation as possible, for example probabilistic or hybrid programs, our definition of transition system will be quite general. When these transition systems are themselves composable - i.e. when one can meaningfully talk about a succession of behaviours - each sequential composition of programs can be represented as a composition of transitions. I will explain how this is an instance of a very important and extensively studied mathematical concept called a "representation". I will argue that this well-known mathematical framework is the natural environment in which to study program semantics abstractly and answer fundamental questions like "given a programming language, what kind of transition systems can interpret all the constructs of this language?", and conversely: "given a class of generalised transition systems, which computations can it support?". I will show some early but exciting results which suggest that this approach could greatly clarify the possible semantics of probabilistic, hybrid or concurrent programs.

Introducing open games

Jules Hedges (Oxford)
Fri, 24th Feb, 14:00 in MSB LT2 (Maurice Shock Building) (Host: Alexander Kurz)

(slides).Open games are a foundation for doing game theory (in the sense of economics, not game semantics) in a compositional way. That is to say, we build games by taking the smallest pieces (such as players and payoff functions) and plugging them together using composition operators, such as simultaneous and sequential play. The result is an algebraic structure called a monoidal category, which inherits an intuitive graphical syntax called string diagrams. To achieve this, open games generalise ordinary games to behave ‘relative to an arbitrary environment’, which behind the scenes uses a sort of continuation passing style.

This will be an introductory talk, not assuming any knowledge of game theory or category theory. I will focus on intuition and examples, and draw as many pictures as possible.

Agent-Based Modelling: Social Science Meets Computer Science?

Edmund Chattoe-Brown (Department of Sociology, Leicester)
Fri, Feb 17, 14:00 in KE LT1 (Host: Alexander Kurz)

(slides). This talk introduces the relatively novel approach of Agent-Based Modelling (hereafter ABM) as a "third way" of representing theories of social behaviour (as distinct from common representations based equations and narratives). Using simple examples, the talk will show how ABM (and particularly its methodology) can make a distinct contribution to social sciences and explores how that contribution might interface with different aspects of computer science.

Inject, Mutate, Improve, Slice – It’s all Testing

Jens Krinke (UCL)
Fri, Feb 10, 14:00 in KE LT1 (Host: Reiko Heckel)

Mutation Testing, Genetic Improvement, and Program Slicing seem to be separate research areas and not necessarily connected to Software Testing. However, they are all based on the principle of drastic changes to the underlying program. This talk will present recent research based on the four areas and how they are connected and which role Software Testing plays.

The scientific life of Ada Lovelace

Ursula Martin (University of Oxford)
Fri, Feb 3, 14:00 in KE LT1 (Host: Rick Thomas)

Ada, Countess of Lovelace (1815-1852) is best known for a remarkable article about Babbage’s unbuilt computer, the Analytical Engine. This not only presented the first documented computer program, but also, going well beyond Babbage’s ideas of computers as manipulating numbers, outlined their creative possibilities and the limits of what they could do. Lovelace’s contribution was highlighted in one of Alan Turing’s most famous papers "Can a machine think?".
The comprehensive archive of Lovelace’s papers preserved in Oxford’s Bodleian Library displays Lovelace’s wide scientific interests in everything from geology to acoustics to chemistry to mesmerism to photography; her exchanges with leading scientists such as Faraday, Babbage and Somerville; her correspondence course in mathematics with De Morgan, a leading mathematician of the day and pioneer in logic and algebra; and her grasp of the potential of mathematics whether to model a "calculus of the nervous system" or as a uniting link between the material and symbolic worlds.
In this talk we start to explore Lovelace, her background, her scientific ideas and her contemporary legacy.

Would the Real Marry Poppins Please Stand Up? Approaches and Methods in Gameful Design

Sebastian Deterding (University of York)
Fri, 27 Jan, 14:00 in KE LT1 (Host: Effie Law, Thomas Erlebach)

(slides) Be it playful design, serious games, gamification, or any other form of applying games and play to serious purposes: It usually takes about five minutes until the Mary Poppins tune “Spoonful of Sugar” is evoked. This talk will explain why this reference is both true and false, how we can indeed find two radically divergent ideas of fun and how to design interfaces in research and practice, how these hold up against current evidence, and how one might go about designing enjoyable interfaces with lessons drawn from games.

Semester 1, 2016/17

Seminar programme

Seminar details

Towards Optimising Energy Consumption Heuristically on Android Mobile Phones

Markus Wagner (University of Adelaide)
Fri, Dec 9, 14:00 in KE LT2 (Host: Leandro Minku)

In this seminar talk, I outline our proposed framework for optimising energy consumption on Android mobile phones. To model the power usage, we use an event-based modelling technique. The internal battery fuel gauge chip or an external meter are used to measure the amount of energy being consumed and accordingly the model is built on. We use the model to estimate components' energy usages. In addition, we propose the use of heuristic optimisation methods to prolong the battery life. This can be achieved by using the power consumption model as a fitness function, re-configuring the smartphone's default settings and modifying existing code of applications.

Inferring Complex In-place Model Transformation Rules

Timo Kehrer (HU Berlin)
Thu, Dec 1, 10:00 in ENG LT1 (Host: Reiko Heckel)

Optimal support for continuous evolution in model-based software development requires tool environments to be customisable to domain-specific modelling languages (DSMLs). An important aspect are the set of change operations available to modify models. In-place model transformations have shown to be well-suited to define model refactorings and other kinds of complex change operations. However, the specification of transformation rules requires a deep understanding of the language meta-model, limiting it to expert tool developers and language designers. This is at odds with the aim of domain-specific visual modelling environments, which should be customisable by domain experts.

This talk reports about ongoing research mitigating this problem, following a model transformation by-example approach: Users generate model transformation rules by creating examples of transformations using standard visual editors as macro recorders. The ambition is to stick entirely to the concrete visual notation domain experts are familiar with, using rule inference to generalise a set of transformation examples. In contrast to previous approaches to the same problem, the proposed approach supports the inference of complex rule features such as negative application conditions, multi-object patterns and global invariants.

Privacy-by-Design Framework for Internet of Things

Charith Perera (Open University)
Fri, Nov 18, 14:00 in KE LT2 (Host: Stephan Reiff-Marganiec)

The Internet of Things (IoT) systems are designed and developed either as standalone applications from the ground-up or with the help of IoT middleware platforms. They are designed to support di erent kinds of scenarios, such as smart homes and smart cities. Thus far, privacy concerns have not been explicitly considered by IoT applications and middleware platforms. This is partly due to the lack of systematic methods for designing privacy that can guide the software development process in IoT. In this talk, I will discuss how we addressed this issue by proposing a set of guidelines, a privacy-by-design framework, that can be used to assess privacy capabilities and gaps of existing IoT applications as well as middleware platforms.

Validation of Decentralised Smart Contracts through Game Theory and Formal Methods

Andrea Bracciali (Stirling)
Thu, Nov 17, 10:00 in ENG LT1 (Host: Emilio Tuosto)

Smart contracts are self-enforcing contracts [1993, Nick Szabo]. In our context, “enforcing” reads as "executable program with (side-) effects", like making a payment. “Self-“, informally speaking, also carries the meaning of "autonomously controlled” or, more specifically, decentralised, not subject to a central authority. Our smart contracts are enabled by blockchains, i.e. decentralised, distributed data structures which can also carry executable code for a non-standard execution environment. The Bitcoin blockchain will discussed to introduce a paradigmatic case of such an execution environment. An example of validation of a smart contract framework, carried out by means of game theory and formal methods, will then be presented. No previous knowledge of bitcoin/blockchain required for this introductory talk .

Aggregation, Opinion-Diffusion, and Liquid Democracy

Davide Grossi (University of Liverpool)
Fri, Nov 11, 14:00 in KE LT2 (Host: Alexander Kurz)

The talk focuses on the issue of aggregation of binary opinions in a group of agents, or judgment aggregation. I will explore some formal interfaces between a special form of aggregation known as proxy voting (aka liquid democracy) and a process of opinion diffusion on networks where each agent’s opinion may be dictated by a (unique) influencer (Boolean DeGroot Processes). The study is an attempt at providing theoretical foundations to liquid democracy, developing a formal framework for its analysis.

This is joint work with Zo Christoff (University of Liverpool).

Requirements-Driven Mediation for Collaborative Security

Amel Bennaceur (Open University)
Nov 4, 14:00 in KE LT2 (Host: Neil Walkinshaw)

Collaborative security exploits the capabilities of the components available in the ubiquitous computing environment in order to protect assets from intentional harm. By dynamically composing the capabilities of multiple components, collaborative security implements the security controls by which requirements are satisfied. However, this dynamic composition is often hampered by the heterogeneity of the components available in the environment and the diversity of their behaviours.

In this talk I will first present an approach for the automated synthesis of mediators that reconcile the differences between the interfaces of the components and coordinate their behaviours from the application down to the middleware layers. Then, I will present a systematic, tool-supported approach for collaborative security based on a combination of feature modelling and mediator synthesis. I will show how we used the FICS (Feature-driven MedIation for Collaborative Security) tool to make two robots—a humanoid robot and a vacuum cleaner—collaborate in order to protect a mobile phone from theft.

Probabilistic formal analysis of software usage styles in the wild

Muffy Calder (cancelled) (University of Glasgow)
Oct 28, 14:00 in KE LT1 (Host: Stephan Reiff-Marganiec)

Discrete mathematics and logics are used to analyse the intended behavior of software systems. Statistical methods are used to analyse the logged data from instrumented systems. So what happens when we instrument software: can we bring the two techniques together to analyse how people actually use software?
But users are difficult to analyse—they adopt different styles at different times! What characterises usage style, of a user and of populations of users, how should we characterise the different styles, how do characterisations evolve over an individual user trace, and/or over a number of sessions over days and months, and how do characteristics of usage inform evaluation for redesign and future design?
I will outline a formal, probabilistic approach based on discrete time Markov chains and stochastic temporal logic properties, applying it to a mobile app that is used by tens of thousands of users worldwide. A new version of the app, based on our analysis and evaluation, has just been deployed. This is formal analysis in the wild!

Computational Social Science: Between Opportunities and Risks

Giuseppe Veltri (University of Leicester)
Oct 21, 14:00 in KE LT1 (Host: Alexander Kurz)

(slides) The contribution of big data and new computational methods to social science is not limited to data collection opportunities but includes the introduction of analytical approaches that have been developed in computer science, and in particular in machine learning. This brings about a new ‘culture’ of statistical modelling that bears considerable potential for the social scientist.
This argument is illustrated with a brief discussion of model-based recursive partitioning which can bridge the theory and data-driven approach. Such a method is an example of how this new approach can help revise models that work for the full dataset: it can be used for evaluating different models, a traditional weakness of the ‘traditional’ statistical approach used in social science.
We will also discuss the role of potential risks in applying new computational methods to social science data without a dialogue between the two research domains.

The scientific life of Ada Lovelace - CANCELLED DUE TO ILLNESS

Ursula Martin (cancelled) (University of Oxford)
Oct 14, 14:00 in KE LT1 (Host: Rick Thomas)

Ada, Countess of Lovelace (1815-1852) is best known for a remarkable article about Babbage’s unbuilt computer, the Analytical Engine. This not only presented the first documented computer program, but also, going well beyond Babbage’s ideas of computers as manipulating numbers, outlined their creative possibilities and the limits of what they could do. Lovelace’s contribution was highlighted in one of Alan Turing’s most famous papers "Can a machine think?".
The comprehensive archive of Lovelace’s papers preserved in Oxford’s Bodleian Library displays Lovelace’s wide scientific interests in everything from geology to acoustics to chemistry to mesmerism to photography; her exchanges with leading scientists such as Faraday, Babbage and Somerville; her correspondence course in mathematics with De Morgan, a leading mathematician of the day and pioneer in logic and algebra; and her grasp of the potential of mathematics whether to model a "calculus of the nervous system" or as a uniting link between the material and symbolic worlds.
In this talk we start to explore Lovelace, her background, her scientific ideas and her contemporary legacy.

Applying Blockchain Technology to Adult Education

John Domingue (Open University)
Oct 7, 14:00 in KE LT1 (Host: Alexander Kurz)

(slideshare or powerpoint) Blockchain is most commonly known as the technology underpinning the Bitcoin cryptocurrency. But in recent years the open source code of the Bitcoin blockchain has been taken and extended by many groups to expand its capabilities. Blockchain technology, which can be thought of as a public distributed ledger, promises to revolutionise the financial world. A World Economic Forum survey in 2015 found that those polled believe that there will be a tipping point for the government use of blockchain by 2023 [1]. Governments, large banks, software vendors and companies involved in stock exchanges (especially the Nasdaq stock exchange) are investing heavily in the area. For example, the UK Government recently announced that it is investing 10M into blockchain research [2] and Santander have identified 20-25 internal use cases for the technology and predict a reduction of banks’ infrastructure costs by up to 12.8 billion a year [3].

The reach of blockchain technology will go beyond the financial sector however, through the use of ‘smart contracts’ which allow business and legal agreements to be stored and executed online. For example, the startup company Tallysticks [4] aims to use blockchain based smart contracts to automate invoicing. In October, 2015 Visa and DocuSign showcased a proof of concept demonstrating how smart contracts could be used to greatly speed up the processes involved in car rental – rental cars can be driven out of the car park without any need to fill in or sign forms. The ability to run smart contracts led Forbes to recently run an article comparing the future impact of blockchains to that of the Web and Internet [5].

In this talk I will give a general overview of blockchains and then describe a number of scenarios that we are working on in the Adult Education domain including certification, ePortfolios and reputation. More information on our work can be found at [6].







Semester 2, 2015/16

Seminar programme

Seminar details

Tracking Data in IoT

Letterio Galletta (Pisa)
Mon 18th July, 14:00 in DW LIB SR David Wilson Library First Floor Library Seminar Room (Host: Emilio Tuosto)

Nowadays smart objects are pervading our everyday life. This scenario is called Internet of Things (IoT). Smart devices are designed to automatically collect and exchange data of various kinds (directly gathered from the physical environment through sensors or obtained as aggregation of other pieces of information). Suitable languages and analysis mechanisms are needed to specify and reason about IoT. In this talk the process calculus IoT-LySa is presented which is endowed with constructs to model this kind of system. Furthermore, IoT-LySa is equipped with a static analysis able to approximate the behaviour of the system and to predict how data gathered from sensors spread and are manipulated inside the network. We also discuss how this output of this analysis can be used to verify some security properties of IoT system.

Stochastic modeling and analysis of congestion control mechanisms with QoS constraints

Lin Guan (Loughborough University)
Fri, Jun 24, 14:00 in ATT LT3 (Host: Thomas Erlebach)

With the rapid development of the Internet, Quality of Service (QoS) has become one of the most important issues in present networks, especially enabling different types of traffic to satisfy specified QoS constraints. This talk will present discrete-time stochastic modelling analysis of a congestion control mechanism for Internet traffic and a new approach for constraining end-to-end delay to a specified value. The feasibility of the system is examined using theoretical analysis, simulation and test-bed.

Differentially Private Policy Evaluation

Borja De Balle Pigem (Lancaster)
Fri June 10, 14:00 in ATT LT3 (Host: Alexander Kurz)

Differential privacy is a mathematical model of privacy which has recently gained a lot of attention within the machine learning community. Essentially, an algorithm operating on a database is differentially private if its output only reveals a small amount of information about any entity in the database. It can be shown that this provides a notion of privacy which is robust against attackers with side knowledge. The first part of this talk will review the basics of differential privacy. In the second part we will present our recent work on differentially private algorithms for policy evaluation in Markov decision processes. Policy evaluation is an important part of reinforcement learning algorithms. In the batch setting, Monte Carlo algorithms for policy evaluation can be formalized using a least squares regression problem with correlated data. Following this approach, we will present two private algorithms for policy evaluation, explain their privacy and utility guarantees, and discuss empirical results on a simple problem that mimics typical applications of Markov decision processes to medical domains.

(Based on our ICML 2016 paper with M. Gomrokchi and D. Precup,

Quantum Structure and the Mathematical Modeling of Human Decision Making

Sandro Sozzo (Leicester)
Fri, May 13, 14:00 in AC LT (Host: Alexander Kurz)

During the last three decades, an increasing number of experimental situations have been identified in cognitive psychology that systematically resist satisfactory modeling by means of traditional classical approaches. For example, effects connected with categorization, such as conceptual vagueness, guppy effect, over- and under-extension in concept combinations, revealed that classical theories, e.g., (fuzzy set) logic and Kolmogorovian probability theory, are structurally incompatible with a possible model for the collected experimental data. Similarly, classical structures were shown to be incompatible with human decision making (prisoner’s dilemma, disjunction effect, conjunction fallacy) and behavioural economics (Ellsberg and Machina paradoxes). The seek of a satisfactory explanation of these non-classical phenomena has led to the development of quantum-based models. Interestingly, quantum models have provided a simple but powerful way to cope with these effects, faithfully modeling empirical data. And more, they have been consistently verified and extended to more complex situations, thus leasing to the configuration of a growing research community, called quantum cognition.

We illustrate here some interesting results we have obtained within our quantum cognition research, with an emphasis on the formalization and representation of natural concepts and their combinations in terms of quantum structures. We firstly show that the data collected on combinations of two concepts cannot generally be modeled in a classical (Kolmogorovian) probability space. Successively, we present a general quantum-theoretic framework that allows faithful modeling of different collections of experimental data on conjunctions, disjunctions and negations of two concepts, including a recent one performed by ourselves. This perspective describes, at the same time, the observed deviations from classical (fuzzy set) logic and probability theory in terms of quantum probability and genuine quantum effects (contextuality, emergence, entanglement and interference). Starting from our successful quantum-theoretic framework, we then formulate a unifying explanatory hypothesis for the above mentioned experimental findings. In it, human reasoning is the superposition of two processes – a conceptual reasoning, whose nature is emergence of new conceptuality, and a logical reasoning, founded on an algebraic calculus of the logical type. We provide arguments to maintain that the former reasoning prevails over the latter in most cognitive processes. Hence, the originally observed experimental deviations from classical logical reasoning should not be interpreted as biases of human mind but, rather, as natural expressions of emergence in its deepest form.

Inspired by this quantum cognition research, we finally illustrate the basics of a quantum meaning based framework for information retrieval (IR) and natural language processing (NLP). The potential advantages of this approach with respect to traditional approaches, such as latent semantic analysis (LSA), are also briefly discussed.

Efficient Large-Scale Graph Processing

Eiko Yoneki (Cambridge)
Fri, May 6, 14:00 in AC LT (Host: Rajeev Raman)

The emergence of big data requires fundamental new methodology for data analysis, processing, and information extraction. The main challenge here is to perform efficient and robust data processing, while adapting to the underlying resource availability in a dynamic, large-scale computing environment. I would introduce our recent work on the graph processing that have billion-scale of vertices and edges in a commodity single computer, which requires secondary storage as external memory. Executing algorithms results in access to such secondary storage and performance of I/O takes an important role, regardless of the algorithmic complexity or runtime efficiency of the actual algorithm in use.

Effects as Sessions, Sessions as Effects

Dominic Orchard (Imperial College London)
Fri, April 29, 14:00 in AC LT (Host: Emilio Tuosto, Alexander Kurz)

Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the λ-calculus and its variants, the latter for the π-calculus. In this talk, I explore their relative expressive power. I'll first give some background for those unfamiliar with either effect systems or session types. Then, I show an embedding from PCF, augmented with a parameterised effect system, into a session-typed π-calculus (session calculus), showing that session types are powerful enough to express effects with linear continuation behaviour. Secondly, I give a reverse embedding, from the session calculus back into PCF , by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result.

This is joint work with Nobuko Yoshida, presented at POPL ’16.

A data-driven, complex networks view of computational search spaces

Gabriela Ochoa (Stirling)
Fri, March 18, 14:00 in AC LT (Host: Leandru Minku)

Computational search is fundamental for solving optimisation problems arising in industry, science and society. A variety of search algorithms have been proposed, but little attention has been devoted to understanding the structure of search spaces. This talk starts by introducing computational search and optimisation using the famous travelling salesman problem as a case study. It then overviews a new model of computational search spaces based on complex networks. Search spaces can be analysed and visualised as complex networks, revealing intriguing structures that shed new light into why some problems are harder to solve than others.

Nominal foundations of mathematics

Jamie Gabbay (Heriot-Watt)
Fri, March 11, 14:00 in AC LT (Host: Alexander Kurz)

Nominal techniques take variable symbols as first-class entities in the mathematical foundations --- so the variable symbol "x" is a first-class primitive datum; and is not represented by e.g. a functional argument or a number. (Technically, "x" is an urelement in Fraenkel-Mostowski set theory.)

It turns out that astonishing richnesses of structure emerge which have been applied: first in the semantics of inductively defined abstract syntax, and then in theorem-proving, concurrency, rewriting, automata theory, and much more.

In recent work I have been applying these ideas to the foundation of mathematics itself. Specifically, I've studied models of three systems in nominal algebra (algebra enriched with names) and nominal powersets (sets of sets enriched with names):

* First-order logic.

* The lambda-calculus.

* Quine's NF.

Using these models I have amongst other things given Stone duality constructions for first-order logic and the untyped lambda-calculus (an open problem), and also a claimed proof of the open problem of the consistency of Quine's NF.

These results are interesting in themselves, they have philosophical significance, and it is clear that the methods used in the proofs are general and interesting, and that the further possibilities are probably extensive.

I will endeavour to deliver an accessible --- that's right: accessible, to the best of my ability! --- guided tour of this material. Technical familiarity will not be required to have a good time.

Courageous or reckless readers can access relevant papers here:,,

Alignment-Free Sequence Comparison: Using Positive and Negative Information

Solon Pissis (King's College London)
Fri, March 4, 14:00 in AC LT (Host: Rajeev Raman)

Sequence comparison is a prerequisite to virtually all comparative genomic analyses. It is often realized by sequence alignment techniques, which are computationally expensive. This has led to increased research into alignment-free techniques, which are based on measures referring to the composition of sequences in terms of their constituent patterns. These measures, such as q-gram distance, are usually computed in time linear with respect to the length of the sequences. In this talk, we visit two recent results: (a) we introduce a new distance measure based on q-grams and show how it can be applied effectively and computed efficiently for circular sequence comparison [WABI 2015]; (b) we focus on the complementary idea: how two sequences can be efficiently compared based on information that does not occur in the sequences. A word is an absent word of some sequence if it does not occur in the sequence. An absent word is minimal if all its proper factors occur in the sequence. We present the first linear-time and linear-space algorithm to compare two sequences by considering all their minimal absent words. In the process, we present results of combinatorial interest, and also extend the proposed techniques to compare circular sequences [LATIN 2016].

Spatial and spatio-temporal model checking

Vincenzo Ciancia (Pisa)
Fri, Feb 26, 14:00 in AC LT (Host: Emilio Tuosto)

So-called spatial logics are a family of logical languages in which some connectives are interpreted according to the characteristics of a mathematical structure representing space. Such languages are aimed at describing properties of points or regions by how they are spatially related to each other. Even though, in principle, spatial reasoning could be applied to several domains, and a plethora of potential practical applications easily come to the mind, so far very few attempts were made in putting such ideas into practice. In this talk, we discuss recent work in implementing spatial reasoning in the form of the model checker “topochecker” for spatial and spatial-temporal logics. We also discuss some ongoing applications of spatio-temporal model checking to analysis of bike sharing systems, medical imaging and computational linguistics.

Developing Interactive Systems for Different Cultures: Issues of Assessing User Experience with Visual Materials

Helen Petrie (York)
Fri, Feb 19, 14:00 in KE LT1 (Host: Effie Law)

Evaluation of user experience (UX) in cross-cultural settings is vital for the development of interactive systems due to the globalization of markets and the search for good user experience in interactive systems. Although interactive systems are distributed globally, users are always local and this should be taken into consideration in methods and materials used in the cross-cultural UX research. A localized web-survey was designed and data collected from 92 respondents in two cultures, Nigeria and Anglo-Celtic (AC) countries (Australia, Canada, Ireland, and the UK). We found that Nigerian respondents are more positive in their ratings than AC respondents, irrespective of content, and are less likely to criticize in their feedback. The culture of the respondents and culture of the visual materials of the scenarios does matter in respondents’ reactions, but the way it matters is not straightforward, and there are complex interactions. We expected that our results would show a strong identification with one’s own cultural group, but this turns out to be only one aspect of a scenario that may affect respondents’ reactions. Therefore care needs to be taken in localizing visual materials and in interpreting the results from different cultural groups.

Privacy in the Large

Pauline Anthonysamy (Google)
Fri, Feb 12, 14:00 in KE LT1 (Host: Ruzanna Chitchyan)

There will be an estimated 35 zettabytes (3510^21) of digital records worldwide by the year 2020. This effectively amounts to privacy management on an ultra-large-scale. In this briefing, we discuss the privacy challenges posed by such an ultralarge-scale ecosystem - we term this “Privacy in the Large”. We will contrast existing approaches to privacy management, reflect on their strengths and limitations in this regard and outline key software engineering research and practice challenges to be addressed in the future.

Formal verification of secure hypervisors

Roberto Guanciale (KTH)
Fri, Feb 5, 14:00 in KE LT1 (Host: Emilio Tuosto)

A hypervisor simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. These systems are used to isolate mission critical components (e.g. cryptoservices) from general purpose (and non-secure) OSs (e.g. Android). For this reason, a security issue in the hypervisor can compromise the security of the complete system. We present our experience in applying formal verification of information flow security for a simple hypervisor for ARMv7. The verification is done by combining interactive theorem proving with analysis tools for binary code.

Scheduling for Electricity Cost in Smart Grid

Prudence Wong (Liverpool)
Fri, Jan 29, 14:00 in KE LT1 (Host: Rob van Stee)

We study a scheduling problem arising in demand response management in smart grid. Consumers send in power requests with a flexible feasible time interval during which their requests can be served. The grid controller, upon receiving power requests, schedules each request within the specified interval. The electricity cost is measured by a convex function of the load in each timeslot. The objective is to schedule all requests with the minimum total electricity cost. In this talk we will consider different variants of this problem, presenting exact algorithms, approximation algorithms and online algorithms.

Semester 1, 2015/16

Seminar programme

Seminar details

Ontology-Based Data Access

Frank Wolter (University of Liverpool)
Fri 11th Dec, 14:00 in BENL LT (Host: Paula Severi, Alexander Kurz)

Ontology-based data access is concerned with querying incomplete data sources in the presence of domain specific knowledge provided by an ontology. A central problem in this setting is that for many classes of ontology and query languages query answering becomes non-tractable. In this talk, I will first introduce ontology-based data access and its applications. Then I will give an overview of weak languages for which query answering is tractable and of the most important techniques for answering queries in this case. Finally, I will discuss non-uniform approaches to understanding the complexity of query answering in ontology-based data access for expressive ontology languages.

Geographic Information and Information Geographies

Stefano De Sabbata (University of Leicester)
Fri 27th Nov, 14:00 in BENL LT (Host: Alexander Kurz)

Information has always had geography. It is from somewhere; about somewhere; it evolves and is transformed somewhere. The first part of the talk will be concerned with the place where geography meets information retrieval and mobile information services. What is special about the spatial component of the data that describe our world, that we store, map, and retrieve? What criteria do we have to take into account when searching for geographic information and how to assess the geographic relevance of information? The second part of the talk will focus on the different geographies of information, and in particular on the geographies of the internet. What factors influence internet access, and how does this reflect on content production? Where does internet content come from, which places are more or less represented, and how does this matter?

Putting the lab on the map: A wireless sensor network system for border security and surveillance

Mohammad Hammoudeh (Manchester Metropolitan University)
Fri 20th Nov, 14:00 in BENL LT (Host: Alexander Kurz)

Traditionally, countries viewed international border control as mostly immigration- and customs-based challenge. However, with the increased risks of terrorism, illegal movement of drugs, weapons, contraband and people, these countries face unprecedented challenges in securing borders effectively. Securing international borders is a complex task that involves international collaboration, deployment of advanced technological solutions and professional skill-sets. In the current financial climate, governments strive to secure their borders, but also ensure that costs are kept low.

Wireless Sensor Networks (WSNs) is a low cost technology that can provide an effective solution to the range of problems faced in securing borders effectively. The ability of a WSN to operate without human involvement and in situations where other surveillance technologies are impractical has made it favourite for deployment in hostile hazardous environments. This technology offers intelligence-led approach to strengthen vulnerable points on the international borders. This class of WSN applications imposes a linear network topology, which has nodes daisy chained using radio communication. Linear WSN topologies are characterised by sparse node deployment, long data transmission distances and alignment of nodes along a virtual line. This talk presents solutions to address the new challenges introduced by Linear WSNs, including: What is the minimum network density to achieve k-barrier coverage in a given belt region? Given an appropriate network density, how to determine if a region is indeed k-barrier covered? How to find a path connecting the two ends of the border such that every point on the path is covered by a sensor node? How to balance workload across sensor nodes? How to elongate network life time and meet quality of service requirements?

Are Semantics and Scalability Incompatible?

Ian Horrocks (University of Oxford)
Fri 13th Nov, 14:00 in BENL LT (Host: Paula Severi)

So called "Semantic Technologies" are rapidly becoming mainstream technologies, with RDF and OWL now being deployed in diverse application domains, and with major technology vendors starting to augment their existing systems accordingly. This is, however, only the first step for Semantic Web research; we need to demonstrate that the Semantic Technologies we are developing can (be made to) exhibit robust scalability if deployments in large scale applications are to be successful. In this talk I will review the evolution of Semantic Technologies to date, and show how research ideas from logic based knowledge representation developed into a mainstream technology. I will then go on to examine the scalability challenges arising from deployment in large scale applications, and discuss ongoing research aimed at addressing them.

Level-based Analysis of Evolutionary Algorithms under Uncertainty

Per Kristian Lehre (University of Nottingham)
Fri 6th Nov, 14:00 in BENL LT (Host: Thomas Erlebach)

Evolutionary algorithms have been applied for decades to tackle hard, real-world optimisation problems in logistics, the automotive industry, the pharmaceutical industry, and elsewhere. Despite their wide-spread use, the theoretical understanding of evolutionary algorithms is still relatively poorly developed. Partly due to lack of methods, time-complexity analysis of evolutionary algorithms have mainly focused on simple algorithms, such as the (1+1) EA which do not use a population or sophisticated genetic operators.

This talk introduces a new method for time-complexity analysis of evolutionary algorithms, the level-based method (Corus et al, PPSN'2014). This method provides upper bounds on the expected hitting times of a wide class of stochastic population models from easy to verify conditions. Level-based analysis has already been applied to study complex algorithms, such as genetic algorithms using crossover, and estimation of distribution algorithms.

As an application of the level-based method, we investigate how evolutionary algorithms cope under different forms of uncertainty in pseudo-Boolean optimisation. We first consider the classical additive noise model, where the objective function is perturbed by a noise term. Secondly, we consider partial evaluation, in which only a random subset of the terms in the objective function are evaluated. The analysis shows that with appropriate settings of mutation rate, selective pressure, and population size, an evolutionary algorithm can cope with surprisingly high levels of uncertainty.

Engineering machine ethics in contemporary artificial intelligence research

Marija Slavkovik (University of Bergen)
Fri 30th Oct, 14:00 in RAT LT (Host: Alexander Kurz)

Machine ethics is an emerging discipline in artificial intelligence research that is concerned with ensuring that the behaviour of machines towards humans and other machines they interact with is ethical. The idea of machine ethics has tickled the fancy of numerous science fictions writers and aficionados, but as of recently, the advancements in robotics and automated systems have shaped this idea into a research topic. Any machine ethics has to be based on human understanding of morality. What kind of autonomous systems should be enhanced with ethical reasoning capabilities? What are the main approaches and challenges to transform vague ideas of right and wrong into machine-comprehensible specifications? Once you get autonomous machines to behave ethically, how can you make sure that they will? How does machine ethics impact other facets of society, or, when a machine misbehaves who is to blame? This talk will explain these questions and the ongoing research efforts towards answering them.

Accent the Positive

Alistair Edwards (University of York)
Fri 23rd Oct, 14:00 in RAT LT (Host: Effie Law)

The way people speak tells a lot about their origins – geographical and social, but when someone can only speak with the aid of an artificial voice (such as Stephen Hawking), conventional expectations are subverted. This seminar will explore some of the limitations and possibilities of speech technology.

Radius of centrality in dynamic networks (or Why grumpy people shouldn't get an ice-cream)

Danica Vukadinovic Greetham (University of Reading)
Fri 16th Oct, 14:00 in RAT LT (Host: Thomas Erlebach)

In this talk, I will look at the problem of centrality ranking in dynamic networks. Centrality is an intuitive concept that tells us how important or involved an individual node is in a network. Many different definitions exist, but not all will work in evolving networks where edges are created and destroyed in each time step. We focus here on one that works well, slightly modified, in evolving networks, Katz centrality, and show how it can be calculated efficiently for relatively large networks.
We then use this calculation to inform a decision on a network based intervention and report the results from several small scale human studies where we observed (and interfered with) the mood dynamics on evolving communication networks.
This is a joint work with Zhivko Stoyanov from Reading and Peter Grindrod from Oxford University.

Calculating wildfire intensity and greenhouse gas emissions using earth observation data

Kirsten Barrett (Department of Geography)
Fri 9th Oct, 14:00 in RAT LT (Host: Alexander Kurz)

The amount of energy emitted by a fire is directly related to the amount of biomass consumed and subsequent emissions of greenhouse gases such as carbon dioxide and methane. Quantifying fire intensity is therefore useful in considering the climate impacts of wildfire disturbance. Optical satellites, which record both reflected and emitted energy (light and heat), can be used to identify where fires are active and how much energy they emit at the time of the overpass. The methods for analysing these data are typical array operations using satellite imagery. Active fires are identified as pixels that are brighter and hotter than the mean of neighboring pixels within a given window. The total amount of energy released by a fire is a function of the intensity at the time of observation, and the duration of a fire within a given pixel. Additional processing allows us to estimate the amount of burning that is likely to be obscured by clouds within an image. Such methods are currently used to estimate global fire emissions, which are estimated to be about half of those from fossil fuels each year.

Semester 2, 2014/15

Seminar programme

Seminar details

Some mathematical aspects of data centre networks

Iain Stewart (Durham)
Fri, May 15, 14:00 in PHY LTA (Host: Rajeev Raman)

The design of data centre networks is becoming an important aspect of computing provision as software and infrastructure services increasingly migrate to the cloud and the demand for bigger and bigger data centres grows. This design is ordinarily undertaken by network engineers and is usually holistic in that not only is an interconnection topology prescribed but more practical aspects are often encompassed relating to, for example, routing, fault-tolerance and throughput. Consequently, these initial designs, though often impressive, tend to be prototypical with the intention being to demonstrate proof-of-concept and practical viability rather than to detail the finished article. Not only does improving and optimizing data centre networks provide opportunities for theoreticians to delve into their mathematical toolboxes but particular aspects of data centre network design can also lead to new problems that perhaps might not be immediately practically relevant but are interesting in their own right from a theoretical perspective. In this talk I shall introduce some of the practical considerations behind data centre network design and show how different aspects of mathematics impinge on this world; such aspects might include isoperimetric sets within graphs, the utilization of combinatorial design theory and the reduction of core data centre problems to combinatorics.

Integer arithmetic with counting quantifiers

Dietrich Kuske (TU Ilmenau)
Fri, Mar 27, 14:00 in PHY LTA (Host: Michael Hoffmann)

We consider Presburger arithmetic (PA) extended with modulo counting quantifiers. We show that its complexity is essentially the same as that of PA, i.e., we give a doubly exponential space bound. This is done by giving and analysing a quantifier elimination procedure similar to Reddy and Loveland's procedure for PA. Furthermore, we show that the complexity of the automata-based decision procedure for PA with modulo counting quantifiers has the same triple-exponential complexity as the one for PA when using least significant bit first encoding. (joint work with Peter Habermehl, LIAFA)

Interaction and causality in digital signature exchange protocols

Jonathan Hayman (Cambridge)
Fri, Mar 20, 14:00 in PHY LTA (Host: Reiko Heckel)

Causal reasoning is a powerful tool in analysing security protocols, as seen in the popularity of the strand space model. However, for protocols that branch, more subtle models are needed to capture the ways in which protocols can interact with a possibly malign environment, for example allowing the expression of security properties of the form ``no matter what the attacker does, the protocol can still achieve a particular goal''.

We study a model for security protocols encompassing causal reasoning and interaction, developing a semantics for a simple security protocol language based on concurrent games played on event structures. We show how it supports causal reasoning about a protocol for secure digital signature exchange. The semantics paves the way for the application of more sophisticated forms of concurrent game, for example including symmetry and probability, to the analysis of security protocols.

Computable analysis and control synthesis of complex dynamical systems via formal verification

Alessandro Abate (Oxford)
Fri, Mar 13, 14:00 in PHY LTA (Host: Nir Piterman)

This talk looks at the development of abstraction techniques based on quantitative approximations, in order to investigate the dynamics of complex systems and to provide computable approaches for the synthesis of control architectures. The approach employs techniques and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on stochastic hybrid systems, which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear). A case study in energy networks, dealing with the problem of demand response, is employed to clarify concepts and techniques.

Multi-Linear Algebraic Semantics for Natural Language

Mehrnoosh Sadrzadeh (Queen Mary)
Fri, March 6, 14:00 in PHY LTA (Host: Alexander Kurz)

Vector spaces offer a contextual way of reasoning about word meanings and have been rather successfully applied to natural language processing tasks. But the basic contextuality hypothesis of these models does not quite work when it comes to phrases and sentences. Herein, one needs to apply Frege's principle of Compositionality and use operations on word vectors to combine them. The high level categorical models of vector spaces (inspired by the work of Abramsky and Coecke on quantum models) have provided a general such setting for compositionality of contextual models.

In this talk, I will present this model (joint work with Clark and Coecke), go over a number of its concrete instantiations, and present experimental results on language tasks (joint work with Grefenstette and Kartsaklis). The latter have outperformed the results of the simple, non-categorical models.

Diagrammatic mathematics and signal flow graphs

Pawel Sobocinski (Southampton)
Fri, Feb 27, 14:00 in PHY LTA (Host: Alexander Kurz)

In recent years there have been a number of developments in the area of symmetric monoidal theories (SMTs), a generalisation of algebraic theories in which one considers operations of arbitrary arity and coarity together with equations, and in which linearity is default: variables cannot be copied and discarded.

String diagrams are an intuitive and powerful graphical syntax for the terms of SMTs. I will report on recent joint work with Filippo Bonchi and Fabio Zanasi, in which, building on the work of Steve Lack on composing SMTs via distributive laws and Yves Lafont on a string-diagrammatic theory of boolean circuits, we discovered the theory of Interacting Hopf Algebras. As well as being closely related to Coecke and Duncan's ZX-calculus for quantum circuits, the associated string diagrams amount to a rigorous and intuitive diagrammatic universe for linear algebra: familiar concepts such as linear transformations and linear spaces appear as certain string diagrams.

As well as giving a new way to look at classical topics in linear algebra, string diagrams sometimes carry useful computational information. I will show how a special case of the theory of Interacting Hopf Algebras captures signal flow graphs, which are a classical circuit notation for linear dynamical systems. When signal flow graphs are considered as string diagrams, diagrammatic reasoning gives a novel, sound and complete technique to reason about them. I will explain how the underlying mathematics leads us to reconsider some popular assumptions about the roles of causality and direction of signal flow, which---in contrast to the primary role traditionally given to them---turn out to be secondary, derived notions: in this way, this work connects with recent trends in control theory, in particular the Behavioural Approach, popularised by Jan Willems.

Sustainable Software Architectures: An Economics-Driven Perspective

Rami Bahsoon (University of Birmingham)
Fri, Feb 21 , 14:00 in ATT LT1 (Host: Stephan Reiff-Marganiec)

The architecture of the system is the first design artifact that realizes the non-functional requirements of the system such as security, reliability, availability, modifiability, real-time performance and their trade-offs. We discuss the challenges in managing change and guiding evolution in large scale software architecture, where uncertainty and dynamism are the norm. We report on ongoing work on evaluating software architectures for sustainability. We posit that the linkage between architectural design decisions, evolution trends of non-functional requirements and sustainability should be explicit; such linkage can provide insights on the success (failure) of software evolution. We argue that one of major indicators of architecture sustainability is the extent to which the architecture design decisions can endure evolutionary changes in non-functional requirements, while continuing to add value. We motivate the need for an economics-driven approach based on the principles of Real Options for valuing software architecture for sustainability. The objective is to assist the architect in strategic “what if” analysis for sustainability involving valuing the flexibility of the architecture to change and/or valuing the worthiness of designing or reengineering for change.

Building dedicated tools

Stephane Ducasse (INRIA)
Fri, Feb 13 , 14:00 in ATT LT1 (Host: Neil Walkinshaw)

In this presentation I will argue for the need of dedicated tools and present the approach developed around Moose ( and engineered in Synectique ( a spinoff of the RMOD group. I will present some industrial cases and the meta tools that we have such as Roassal, Glamour.

Signal processing helping cure cardiac arrhythmias

Fernando Schlindwein (Bioengineering Research Group, University of Leicester)
Fri, Feb 6 , 14:00 in ATT LT1 (Host: Alexander Kurz)

Atrial Fibrillation is the most common cardiac arrhythmia. Patients with AF are five times more likely to have a stroke. We are going to show how using real-time signal processing can help cure AF using catheter ablation of the areas responsible for the generation or maintenance of AF.

Is Modeling Any Good? Empirical Evidence on Modeling of Design in Software Development

Michel Chaudron (Chalmers)
Fri, Jan 30, 14:00 in ATT LT1 (Host: Reiko Heckel)

(Slides) Modeling is a common part of modern day software engineering practice. Little evidence is known about how models are used and if/how they help in producing better software. In this talk I will present highlights from the last decade of research in the area of modeling software designs using UML. Topics that will be addressed in this talk are:

- What is the state of UML modeling in practice?

- How can we assess the quality of UML models?

- Does UML modelling actually help in creating better software?

- If time permits, I will show some snapshots of ongoing research in these areas.

Semester 1, 2014/15

Seminar programme

Seminar details

From Communicating Machines to Graphical Choreographies

Julien Lange (Imperial College London)
12th Dec, 14:00 in GP LTB (Host: Emilio Tuosto)

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In this talk, I will present (i) an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and (ii) a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed.

On state space problems when designing languages with relaxed consistency in Maude

Alberto Lluch Lafuente (Technical University of Denmark)
5th Dec, 14:00 in GP LTB (Host: Emilio Tuosto)

Memory consistency is sometimes given up for the sake of performance both in concurrent and in distributed systems. Operational models of consistency relaxations like relaxed memory models offer suitable abstractions that can be used for various purposes (e.g. verification) but pose some challenges in state space exploration activities (e.g. verification) in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make the analysis of programs under relaxed consistency feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar state space exploration purposes.

Toward a Comprehensive Framework for Business Process Compliance

Amal Elgammal (Trinity College Dublin)
4th Dec, 10:00 in BEN LT (Host: Artur Boronat)

Today's enterprises demand a high degree of compliance of business processes to meet ‎regulations, such as Sarbanes-Oxley and Basel III. To ensure continuous guaranteed ‎compliance, it should be enforced during all phases of the business process lifecycle, from the ‎phases of analysis and design to deployment, monitoring and adaptation. This course of ‎research primarily concentrates on design-time aspects of compliance management and ‎secondarily on business process runtime monitoring; hence, providing preventive lifetime ‎compliance support. While current manual or ad-hoc solutions provide limited assurances ‎that business processes adhere to relevant constraints, there is still a lack of an established ‎generic framework for managing these constraints; integrating their relationships and ‎maintaining their traceability to sources and processes; and automatically verifying their ‎satisfiability. In this talk, I will present my research results that address the problems of automating the compliance verification activities during design-time and the reasoning and analysis of detected compliance violations.

Choreographies in the wild

Massimo Bartoletti (University of Cagliari)
28th Nov, 14:00 in GP LTB (Host: Emilio Tuosto)

Distributed applications can be constructed by composing services which interact by exchanging messages according to some global communication pattern, called choreography. Under the assumption that each service adheres to its role in the choreography, the overall application is communication-correct.

However, in wild scenarios like the Web or cloud environments, services may be deployed by different participants, which may be mutually distrusting (and possibly malicious). In these cases, one can not assume (nor enforce) that services always adhere to their roles.

Many formal techniques focus on verifying the adherence between services and choreographic roles, under the assumption that no participant is malicious; in this case, strong communication-correctness results can be obtained, e.g. that the application is deadlock-free. However, in wild scenarios such techniques can not be applied.

In this talk we present a paradigm for designing distributed applications in wild scenarios. Services use contracts to advertise their intended communication behaviour, and interact via sessions once a contractual agreement has been found. In this setting, the goal of a designer is to realise honest services, which respect their contracts in all execution contexts (also in those where other participants are malicious).

A key issue is that the honesty property is undecidable in general. In this talk we discuss verification techniques for honesty, targeted at agents specified in the contract-oriented calculus CO2. In particular, we show how to safely over-approximate the honesty property by a model-checking technique which abstracts from the contexts a service may be engaged with.

Logical Foundations for Session-Based Concurrency: Overview and Recent Developments

Jorge Perez (Groningen, The Netherlands)
21st Nov, 14:00 in GP LTB (Host: Paula Severi, Alexander Kurz)

(based on joint works with Luis Caires, Frank Pfenning, and Bernardo Toninho) A central concept in the theory of programming languages is the so-called Curry-Howard isomorphism: it tightly relates, on the one hand, logical propositions and types; on the other hand, it connects proofs and functional programs. This isomorphism has proved essential to endow reasoning techniques over sequential programs with clean principles, which have both operational and logical meanings.

In 2010, Caires and Pfenning put forward an interpretation of linear logic propositions as session types for communicating processes. Remarkably, this result defines a propositions-as-types/proofs-as-programs correspondence, in the style of the Curry-Howard isomorphism, but in the context of concurrent processes defined in the pi-calculus.

In this talk, I will give an overview to Caires and Pfenning's interpretation, from the perspective of languages for concurrency. I will also present some associated developments, which complement the interpretation by Caires and Pfenning: logical relations, typed behavioral equivalences, and type isomorphisms.

If time permits, I will discuss two further developments. The first concerns the analysis of choreographies (multiparty protocols defined by session types) using the type discipline induced by Caires and Pfenning's interpretation. The second result extends the Caires and Pfenning's interpretation to a domain-aware setting, relying on a linear logic augmented with "worlds" from hybrid logic, here interpreted as distributed locations (or sites).

Encodings of Range Maximum-Sum Segment Queries and Applications

Pat Nicholson (MPI Saarbruecken)
7th Nov, 14:00 in GP LTB (Host: Rajeev Raman)

Given an array A containing arbitrary (positive and negative) numbers, we consider the problem of supporting range maximum-sum segment queries on A: i.e., given an arbitrary range [i,j], return the subrange [i' ,j' ] ⊆ [i,j] such that the sum of the numbers in A[i'..j'] is maximized. Chen and Chao [Disc. App. Math. 2007] presented a data structure for this problem that occupies Θ(n) words, can be constructed in Θ(n) time, and supports queries in Θ(1) time. Our first result is that if only the indices [i',j'] are desired (rather than the maximum sum achieved in that subrange), then it is possible to reduce the space to Θ(n) bits, regardless the numbers stored in A, while retaining the same construction and query time. We also improve the best known space lower bound for any data structure that supports range maximum-sum segment queries from n bits to 1.89113n bits. Finally, we provide a new application of this data structure which simplifies a previously known linear time algorithm for finding k-covers: i.e., given an array A of n numbers and a number k, find k disjoint subranges [i_1 ,j_1 ],...,[i_k ,j_k ], such that the total sum of all the numbers in the subranges is maximized.

APEX: An Analyzer for Open Probabilistic Programs

Andrzej Murawski (University of Warwick)
31st Oct, 14:00 in ATT LT1 (Host: Thomas Erlebach)

We present APEX, a tool for analysing probabilistic programs that are open, i.e. where variables or even functions can be left unspecified. APEX transforms a program into an automaton that captures the program’s probabilistic behaviour under all instantiations of the unspecified components. The translation is compositional and effectively leverages state reduction techniques. APEX can then further analyse the produced automata; in particular, it can check two automata for equivalence which translates to equivalence of the corresponding programs under all environments. In this way, APEX can verify a broad range of anonymity and termination properties of randomised protocols and other open programs, sometimes with an exponential speed-up over competing state-of-the-art approaches.

This is joint work with S. Kiefer, J. Ouaknine, B. Wachter and J. Worrell.

Measuring User Experience in Human-Computer Interaction: Current status, caveats and alternative methods

Anders Bruun (Aalborg University)
24th Oct, 14:00 in ATT LT1 (Host: Effie Law)

The concept of User Experience (UX) in Human-Computer Interaction has evolved over the past 10 years. UX is typically considered to cover a broad range of dimension going beyond usability of interactive products. This talk will firstly provide a brief overview of state-of-the art in UX research. Secondly, the talk will present results from a recent experiment questioning the reliability of current practices for assessing UX.

UX is typically measured retrospectively through subjective questionnaire ratings, yet we know little of how well these retrospective ratings reflect concurrent experiences of an entire interaction sequence. The talk will present findings from an empirical study of the gap between concurrent and retrospective ratings of UX. Alternative methods of assessing UX will be discussed, which have considerable implications for practice.

Hansel and Gretel: Connecting the dots of evidences via provenance trails

Jun Zhao (Lancaster University)
17th Oct, 14:00 in ATT LT1 (Host: Ruzanna Chitchyan)

Scientific integrity is facing growing scrutiny. We read more and more high profile stories about scientific ‘flaws’ and embarrassment, which not only have serious impact on the life of generations but also that of the scientists themselves. All of these have recently led to serious doubts about the significance of the results and quality of the peer-review process, with peer review costing an estimated $2 billion US dollars each year.

Provenance information records where a data item came from and how it was produced. A driving theme in provenance research is to understand how best to use provenance as the critical evidence to support scientists justifying and validating their findings and improve the efficiency and efficacy of the peer review process.

In this talk, I will discuss the role of provenance research in enhancing reproducibility of computational research and examine the critical gap in existing provenance research for fulfilling this goal. I will outline our approach of applying semantic web technologies to provenance data mining and argue an important role to be played by data mining technologies in provenance data analytics at a large scale.

The Power of Mobile Sensing and its Applications

Cecilia Mascolo (University of Cambridge)
10th Oct, 14:00 in ATT LT1 (Host: Thomas Erlebach)

In this talk I will describe our research in the area of mobile sensing and mobile phone sensing. I will introduce a variety of projects which we have conducted to monitor people’s mobility and behaviour with handheld devices as well as embedded technology. I will introduce the challenges related to mobile sensing and the solutions which we have proposed in terms of power preservation and behaviour inference. The specific studies described include Emotion Sense, a platform to monitor mood and behaviour for psychological studies, our work on using location and accelerometer data to understand parking and driving patterns and a study using RFID technology to monitor interaction and use of space in buildings.

Fast Statistical Assessment for Combinatorial Hypotheses Based on Frequent Itemset Enumeration

Shin-Ichi Minato (Hokkaido University, Japan)
Fri, 19th Sept, 13:00 in Bennett LT5 (Host: Rajeev Raman)

In many scientific communities using experiment databases, one of the crucial problems is how to assess the statistical significance (p-value) of a discovered hypothesis. Especially, combinatorial hypothesis assessment is a hard problem because it requires a multiple-testing procedure with a very large factor of the p-value correction. Recently, Terada et al. proposed a novel method of the p-value correction, called "Limitless Arity Multiple-testing Procedure" (LAMP), which is based on frequent itemset enumeration to exclude meaninglessly infrequent itemsets which will never be significant. The LAMP makes much more accurate p-value correction than previous method, and it empowers the scientific discovery. However, the original LAMP implementation is sometimes too time-consuming for practical databases. We propose a new LAMP algorithm that essentially executes itemset mining algorithm once, while the previous one executes many times. Our experimental results show that the proposed method is much (10 to 100 times) faster than the original LAMP. This algorithm enables us to discover significant p-value patterns in quite short time even for very large-scale databases.

Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356.
University of Leicester . Last modified: 16th May 2017, 07:47:49.
Informatics Web Maintainer. This document has been approved by the Head of Department.