Computer Science Seminars

Note: This page shows past seminars up to 2017/18 Semester 2. Upcoming seminars can be found here.

Semester 2, 2017/18

Seminar programme

Seminar details

Carlos Gustavo Lopez Pombo (University of Buenos Aires)
Thu, 19th July, 14:00 in tba (Host: Emilio Tuosto)

Distributed software resulting from emerging paradigms such as service- oriented computing (SOC), Cloud/Fog computing and the Internet of Things are transforming the world of software systems in order to support applications able to respond and adapt to the changes of their execution environment, giv- ing impulse to what is called the API’s economy. The underlying idea of the API’s economy is that it is possible to construct software artifacts by compos- ing services provided by third parties and previously registered in repositories. This envisages a generation of applications running over globally available com- putational resources and communication infrastructure, which, at run-time, are dynamically and transparently reconfigured by the intervention of a dedicated middleware, subject to the negotiation of a Service Level Agreement – SLA.

Asynchronous Relational Nets is a language for describing the orchestration of services, supporting the explicit dynamic reconfiguration of a system by declaring ports behaving either as provide points or as require points, depending on their role in the service binding and execution. In a previous work we used Communicating Finite State Machine to label provides points and while communication channels where labeled with Global graphs, in order to describe a procedure for automatically checking interoperability of services.

In this talk we present: 1) a new class of CFSMs, called Multichannel Communicating Finite State Machines – mCFSMs, with an explicit definition of the communication channels enabling, for a participant, the possibility of having more than one channel with the other participants 2) a definition of the multiparty compatibility property for systems of mCFSMs, 3) a class of Asynchronous Communicating Automata – ACAs with the capability of internalising the communication as read / write operations on internal buffers, enabling partial composition of communicating automata, and 4) a method for mapping an ACA to a mCFSM providing a checking mechanism of the GMC property for the class of ACA.

Prakash Panangaden (McGill University and the Alan Turing Institute)
Fri, 22nd June, 14:00 in ATT 001 (Host: Alexander Kurz)

Reasoning with equations is a central part of mathematics. Typically we think of solving equations but another role they play is to define algebraic structures like groups or vector spaces. Equational logic was formalized and developed by Birkhoff in the 1930s and led to a subject called universal algebra. Universal algebra was used in formalizing concepts of data types in computer science. In this talk I will present a quantitative analogue of equational logic: we write expressions like s =_ε t with the intended interpretation "s is within ε of t". It turns out that the metatheory of equational logic can be redeveloped in this setting. Perhaps this seems like sterile theory but what makes it come alive is some striking examples. A notion of distance between probability distributions called the Kantorovich metric (frequently called the Wasserstein metric) has become important in the theory of probabilistic systems and in parts of machine learning. It turns out that this metric emerges naturally as the "free algebra" of some simple equational axioms in our extended sense. This is joint work with Radu Mardare and Gordon Plotkin.

Fernando Orejas (Universitat Politecnica de Catalunya)
Thu, June 7, 13:00 in ATT 002 (Host: Reiko Heckel)

Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about the properties that a given graph may or may not satisfy. In particular, our work is motivated by model-driven software development and by graph data bases. With this aim, in this seminar I will present a visual logic that allow us to describe graph properties, including properties about paths (for this reason, we have called the logic "navigational") . The logic is equipped with a deductive tableau method that we have proved to be sound and complete. Moreover, we have shown that this logic is an institution.

Luigi Novella (Universita degli Studi del Sannio)
Wed, 6th June, 14:00 in ATT 208 (Host: Neil Walkinshaw)

The integrity and reliability of reactive systems are very important and, in order to ensure them, an intensive testing procedure is required. Testing with model learning tries to address the limitations of model based testing by learning a model of the system under test as testing is performed.

This talk will concern with the challenge of automatically producing test sets for black-box systems and will describe a novel testing with model learning technique to achieve functional coverage and test depth in the absence of specifications.

The approach’s effectiveness will be demonstrated in the event-based GUI testing process of Android applications.

Pawel Sobocinski (University of Southampton)
Fri, May 11, 14:00 in ATT 208 (Host: Alexander Kurz)

In his recent seminar at Leicester, Fabio Zanasi talked about working with string diagrams as an intuitive and powerful notation, with several different applications in computer science and related disciplines. In order to arrive at an implementation of diagrammatic reasoning, one needs a suitable data structure to represent them. In a LiCS'16 paper with Bonchi, Gadducci, Kissinger and Zanasi, we identified this as hypergraphs-with-interfaces, or---categorically speaking---discrete cospans of hypergraphs. This combinatorial presentation has the core of diagrammatic reasoning (i.e. the laws of symmetric monoidal categories) built in, and is therefore useful especially for rewriting, which reduces to double-pushout graph rewriting. In general, connections between categorical structures and combinatorial structures are often extremely useful.

In this talk I will argue that there is one important actor missing from the above story: logic. In recent work (arXiv:1804.07626) with Bonchi and Seeber, we identified a deep connection with a foundational logical calculus from database theory, the Calculus of Conjunctive Queries. Moreover, we showed that the algebraic theory of cartesian bicategories (Carboni and Walters) captures the notion of query inclusion. A classical result by Chandra and Merlin states that query inclusion is decidable: we derive this decidability result through a deep triangular relationship between categorical structure (cartesian bicategories), logic (conjunctive queries) and combinatorics (hypergraphs-with-interfaces).

Jian Liu (Centre for Systems Neuroscience, University of Leicester)
postponed, in (Host: Huiyu (Joe) Zhou)

The retina is the first stage of visual processing in the brain. However, how natural scenes are encoded by retinal ganglion cells (RGCs) is still unsolved. Here, I will discuss this topic by studying the recorded RGC spiking responses. We developed some data-driven approaches, spike-triggered non-negative matrix factorization and deep learning nets for characterizing the underlying mechanisms of retinal visual processing. I further demonstrate that how these computational principles of neuroscience can be translated to neuromorphic chips for the next generation of the artificial retina to enhance the performance of neuroprosthesis and neurorobotics.

(by Simon Thompson and Pablo Lamela Seijas) This seminar will describe our current work in designing domain-specific languages to describe contracts that run on blockchains. We'll present a prototype DSL, Marlowe, implemented in Haskell, and discuss the design choices made in defining it, as well as the next steps of our work. We'll begin with introductions to blockchain and scripting, so that it should be accessible to a wider audience.

Diagrammatic languages are used in diverse fields of science to specify and study systems based on interacting components. Graphics outperforms textual information in highlighting connectivity and resource-exchange between parts of a system. This makes diagrammatic languages particularly effective in the analysis of subtle interactions as those found in cyber-physical, concurrent and quantum systems.

In recent years "algebraic network theory" emerged in theoretical computer science as a unifying mathematical framework in which diagrammatic languages are given a completely formal status and are studied using the compositional methods of algebraic program semantics. Nowadays the algebraic approach founds application in fields as diverse as quantum theory, linguistics, Bayesian probability, concurrency theory and the analysis of signal processing, electrical and digital circuits.

In this talk we give a general overview of the field and show some recent advances, especially in regard to signal processing theory and Bayesian reasoning.

I will present recent and ongoing work, based on automata and session types, towards supporting the verification of real-world time-sensitive programs. The talk will centre on a theory of refinements for timed asynchronous systems, in the formal setting of Communicating Timed Automata. I will introduce three notions of (compositional and decidable) refinement, serving as a formal counter-part of concrete implementations with time-sensitive programming primitives. I will then establish conditions under which the given refinements preserve the behaviour of systems and their progress properties. All our results build upon new semantics of CTAs, that are needed to faithfully model the behaviour of real-time primitives of mainstream programming languages. I will discuss how these results fit in the context of developing effective tools for design and development of time-sensitive systems.

Simone Stumpf (Centre for HCI Design, City, University of London)
Fri 2 Feb, 14:00 in KE LT1 (Host: Effie Law)

Smart systems that apply complex reasoning to make decisions and plan behaviour, such as clinical decision support systems, personalised recommendations, home automation, machine learning classifiers, robots and autonomous vehicles, are rapidly becoming part of everyday user interaction. It has been shown that users need to understand how an intelligent system works in order to use it effectively, promote positive attitudes towards the system, increase their trust in the system's decisions, and to gain a sense of controllability, yet so far most of these systems are like black boxes and not at all transparent. My research has focused on providing explanations – textual and graphical – of the behaviour of intelligent user interfaces. In this talk I will provide an overview of previous work and a current project that investigates explanations for smart heating systems.

William Darler (School of Business – Marketing Division, University of Leicester)
Fri 26 Jan, 14:00 in KE LT1 (Host: Leandru Minku)

Researchers and practitioners have long been interested in how human behaviour changes over time. Events that happen in the course of a person’s life can often lead to changes in consumption behaviour and interactions with the marketplace. Although consumer behaviour during life events has received much attention in marketing literature, there has been little research carried out using real world transaction data and time has often been a neglected component. This rise in availability of big data sets and surge of interest in machine learning techniques allows us to understand consumer behaviour at a more granular level than ever before. We use transaction data from over 3.5 million customers of a multinational retailer and a supermarket to understand how consumer behaviour changes during life events. In our research, we created two new methods (i) To identify the times at which consumer behaviour changes during a life event, and (ii) To segment customers based on their behavioural trajectories. Our research contributes to life course theory and is useful to practitioners for gaining a greater understanding of their customers and planning marketing activities.

I would also like to talk about some other data-driven projects I am currently involved with in the following industries: sports, video gaming, natural disasters, automotive, NHS/air quality, retail.

I would like to invite all the attendees to join me for cake at the University of Leicester Innovation Hub after my talk and meet some of the staff there who deal with a range of projects and are keen to meet people from Informatics.

Semester 1, 2017/18

Seminar programme

Seminar details

Tracy Hall (Brunel University London)
Fri, Dec 1, 14:00 in BEN LT1 (Host: Leandro Minku)

This presentation introduces software defect prediction and in particular mutation-aware defect prediction. This new approach leverages additional guidance from mutation testing in the form of metrics constructed in terms of mutants and the test cases that cover and detect them. Mutation-aware defect prediction can significantly (p ≤ 0.05) improve defect prediction performance. The results of 12 sets of experiments are reported, applying 4 different predictive modelling techniques to 3 large real-world systems (both open and closed source). Mutation metrics lie in the top 5% most frequently relied upon defect predictors in 10 of the 12 sets of experiments, and provide the majority of the top ten defect predictors in 9 of the 12 sets of experiments.

The presentation is based on: David Bowes, Tracy Hall, Mark Harman, Yue Jia, Federica Sarro, and Fan Wu. 2016. Mutation-aware fault prediction. In Proceedings of the 25th International Symposium on Software Testing and Analysis (ISSTA 2016).

In combinatorics of words, a concatenation of k consecutive equal blocks (factors) is called a power of order k. In this talk we present a different point of view and define an anti-power of order k as a concatenation of k consecutive pairwise distinct blocks of the same length. We show that every infinite word must contain powers of any order or anti-powers of any order. We also discuss some other questions related to the definition of anti-power.

In collaboration with A. Restivo, M. Silva and L. Zamboni.

Uli Sattler (University of Manchester)
Fri, Nov 3, 14:00 in BEN LT1 (Host: Paula Severi, Alexander Kurz)

Description Logics (DLs) are (mainly) decidable fragments of First Order Logic designed to capture domain knowledge for knowledge-intensive application. They form the logical basis of ontology languages like OWL, whose standardisation has led to the development of a variety of tools, APIs, and IDEs which, in turn, have led to the development and use of large ontologies and interesting ontology-based applications. This development has given rise to a number of interesting logic-related questions, some of which are closely related to standard automated reasoning problems. In this talk, I want to give a flavour of what DLs, OWL, and ontologies are about, how they are used, and what these logic-related questions are (both the standard and the non-standard ones).

Atze Dijkstra (Strats team, Standard Chartered Bank)
27 October, 14:00 in BEN LT1 (Host: Alexander Kurz)

In an enterprise setting use of tools to reduce software and development complexity while keeping maintenance manageable is a key ingredient for achieving success. In this talk we show how Haskell plays a large role in how the Strats team at Standard Chartered delivers software, correct and on time. Besides pointing out useful language features we also demonstrate by example how some of these language features are used.

Muffy Calder (University of Glasgow)
20 October, 14:00 in BEN LT1 (Host: Stephan Reiff-Marganiec)

How do users actually interact with software? If we can answer that, then perhaps we can (re)-design better systems.

But users are heterogeneous: they adopt different usage styles and each individual user may move between different styles, from one interaction session to another, or even during an interaction session. We require new temporal analytics: techniques to model and analyse temporal data sets of logged interactions with the purpose of discovering, interpreting, and communicating meaningful patterns of usage.

This talk outlines a new temporal analytics and applies it to a mobile app that has been used by tens of thousands of users worldwide. We re-designed the app based on analysis results, and released the new version last year. This is formal analysis in the wild! The talk is aimed at a general computer science audience.

Alexander Gorban (Department of Mathematics, University of Leicester)
13 October, 14:00 in BEN LT1 (Host: Alexander Kurz)

(Joint work wit Ivan Tyukin and Evgeny Mirkes)

We study multi-agent neural networks. An agent submits a solution for each task together with the self-esteem. The self-esteem measures how sure it is about this answer. The problem space is separated between the agents during training. A trained agent solves the problems in his areas correctly and with high self-esteem. The problems which are owned by another agents are either solved correctly or incorrectly but with low self-esteem. Such network can develop and learn further by knowledge transfer between agents in a semi-supervised manner. Distribution of the problems between agents could be also presented in a form of a special adaptive coding neural network. The social networks of neural agents are universal tools for problem solving.

The knowledge transfer between agents is based on recently discovered Stochastic Separation Theorems and on one-shot correctors of mistakes. The problem of non-iterative one-shot and non-destructive correction of unavoidable mistakes arises in all Artificial Intelligence applications in the real world. Its solution requires robust separation of samples with errors from samples where the system works properly. Stochastic separation theorems demonstrate that in (moderately) high dimension this separation could be achieved with probability close to one by linear discriminants.

E-prints partially presented the topic and include some preliminary material:

https://arxiv.org/pdf/1703.01203.pdf

https://arxiv.org/pdf/1610.00494.pdf

https://arxiv.org/pdf/1709.01547.pdf

In this talk, I'll focus on three contexts in which people regularly multitask while using computers: driving a car, doing work tasks, and relaxing on the sofa at home. Across these contexts, I shall describe how we have used different research methods and approaches to understand how people multitask: from cognitive modelling, to control lab experiments, to situated observational studies, and online studies with crowdsourcing platforms. This research helps us understand why some people are better at multitasking than others, and how systems can be designed to help us focus our attention when we need to.

Semester 2, 2016/17

Seminar programme

Seminar details

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.

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

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.

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

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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 .

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).

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.

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!

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.

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].

1. http://www.coindesk.com/world-economic-forum-governments-blockchain

2. https://www.cryptocoinsnews.com/the-uk-treasury-is-embracing-block-chain-digital-currencies-and-big-data-research

3. http://uk.businessinsider.com/santander-has-20-25-use-cases-for-bitcoins-blockchain-technology-everyday-banking-2015-6

4. http://tallysticks.io/

5. http://www.forbes.com/sites/valleyvoices/2015/12/21/why-the-blockchain-is-the-new-website/#2715e4857a0b742d9a29ac2e

6. Blockchain.open.ac.uk

Semester 2, 2015/16

Seminar programme

Seminar details

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.

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.

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, http://arxiv.org/abs/1603.02010)

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.

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.

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.

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.

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: www.gabbay.org.uk/papers.html#semooc, www.gabbay.org.uk/papers.html#repdul, www.gabbay.org.uk/papers.html#conqnf.

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].

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.

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.

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

There will be an estimated 35 zettabytes (35×10^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.

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.

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

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.

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?

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?

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.

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.

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.

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.

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.

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

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.

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)

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.

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.

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.

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.

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.

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 (http://www.moosetechnology.org) and engineered in Synectique (http://www.synectique.eu) a spinoff of the RMOD group. I will present some industrial cases and the meta tools that we have such as Roassal, Glamour.

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.

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

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.

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.

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.

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 veriﬁcation 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.

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).

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.

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.

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.

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.

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.

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.

	cms
	HOME	MAP	CONTACT

Up University Home Science & Engineering Informatics Home University A-Z
Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356. © University of Leicester . Last modified: 2nd September 2018, 21:51:19 CMS Web Maintainer. This document has been approved by the Head of Department.

cms