ABOUT 
Computer Science SeminarsUseful links:
Semester 2, 2017/18Seminar programme
Seminar detailsQuantitative equational reasoning
Prakash Panangaden (McGill University and the Alan Turing Institute) 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.
A navigational logic for reasoning about graphs
Fernando Orejas (Universitat Politecnica de Catalunya) 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 modeldriven 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) 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 blackbox 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 eventbased GUI testing process of Android applications.
Pawel Sobocinski (University of Southampton) 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 hypergraphswithinterfaces, orcategorically speakingdiscrete 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 doublepushout 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 (hypergraphswithinterfaces).
Retinal computation: neuroscience, neuroprosthesis and neurorobotics
Jian Liu (Centre for Systems Neuroscience, University of Leicester) 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 datadriven approaches, spiketriggered nonnegative 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.
Marlowe: financial contracts on blockchain
Simon Thompson (Kent) (by Simon Thompson and Pablo Lamela Seijas)
This seminar will describe our current work in designing
domainspecific 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.
Algebraic methods for network diagrams and componentbased systems
Fabio Zanasi (UCL) 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 resourceexchange between parts of
a system. This makes diagrammatic languages particularly effective in the analysis of subtle interactions as those found in
cyberphysical, 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.
From timesensitive models to timesensitive programs
Laura Bocchi (Kent) I will present recent and ongoing work, based
on automata and session types, towards supporting the
verification of realworld timesensitive 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 counterpart of concrete implementations with
timesensitive 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 realtime primitives of
mainstream programming languages. I will discuss how these
results fit in the context of developing effective tools for
design and development of timesensitive systems.
Explaining smart systems to encourage (or discourage?) user interaction (slides)
Simone Stumpf (Centre for HCI Design, City, University of London) 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.
A time to change: a data driven approach to consumer behaviour and trajectories during life events
William Darler (School of Business – Marketing Division, University of Leicester) 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 datadriven 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/18Seminar programme
Seminar detailsMutationAware Defect Prediction
Tracy Hall (Brunel University London) This presentation introduces software defect prediction and in particular mutationaware 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. Mutationaware 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 realworld 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. Mutationaware fault prediction. In Proceedings of the 25th International Symposium on Software Testing and Analysis (ISSTA 2016).
Antipowers in words: a new notion of regularity based on diversity
Gabriele Fici (Palermo) 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 antipower 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 antipowers of any order. We also discuss some other
questions related to the definition of antipower.
In collaboration with A. Restivo, M. Silva and L. Zamboni.
Description Logics, Ontologies, and OWL
Uli Sattler (University of Manchester) Description Logics (DLs) are (mainly) decidable fragments of First Order Logic designed to capture domain knowledge for knowledgeintensive 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 ontologybased applications. This development has given rise to a number of interesting logicrelated 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 logicrelated questions are (both the standard and the nonstandard ones).
Haskell in the Large  Exploiting Haskell to manage software complexity
Atze Dijkstra
(Strats team, Standard Chartered Bank)
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.
Temporal analytics of software usage styles in the wild
Muffy Calder
(University of Glasgow) 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 redesigned 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.
Selfesteem and Social Networks of Neural Networks
Alexander Gorban
(Department of Mathematics, University of Leicester) (Joint work wit Ivan Tyukin and Evgeny Mirkes)
We study multiagent neural networks. An agent submits a
solution for each task together with the selfesteem. The
selfesteem 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 selfesteem. The problems which are
owned by another agents are either solved correctly or
incorrectly but with low selfesteem. Such network can develop
and learn further by knowledge transfer between agents in a
semisupervised 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 oneshot correctors of
mistakes. The problem of noniterative oneshot and
nondestructive 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. Eprints 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
Multitasking in HumanComputer Interaction
Duncan Brumby
(UCL)
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/17Seminar programme
Seminar detailsComputing continuoustime Markov chains as transformers of unbounded observables
Tobias Heindl (University of Leipzig) The talk describes continuoustime Markov chains
(CTMCs) as transformers of realvalued 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 substring occurrences of stochastic string rewriting
systems. The result provides a functional analytic alternative
to Monte Carlo simulation as test bed for meanfield
approximations, moment closure, and similar techniques that
are fast, but lack absolute error guarantees.
Peter Thiemann (Universitaet Freiburg) 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, webbased
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
sessionbased 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)
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.
Selfesteem and Social Networks of Neural Networks
Alexander Gorban (talk postponed) (Department of Mathematics, Leicester) Knowledge Transfer Between AI Systems
Ivan Tyukin (Department of Mathematics, Leicester)
(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
retraining 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 viceversa. 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 ndimensional topological vector space, b)
preexisting 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 noniteratively 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 pretrained convolutional neural network and
2) from a pretrained convolutional neural network to a simple
linear HOGSVM classifier.
A metatheory of program semantics
Fredrik Dahlqvist (University College London) 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 wellknown 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)
(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.
AgentBased Modelling: Social Science Meets Computer Science?
Edmund ChattoeBrown (Department of Sociology, Leicester)
(slides). This talk introduces the relatively novel
approach of AgentBased 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) 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) Ada, Countess of Lovelace (18151852) 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)
(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/17Seminar programme
Seminar detailsTowards Optimising Energy Consumption Heuristically on Android Mobile Phones
Markus Wagner (University of Adelaide) 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 eventbased
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, reconfiguring
the smartphone's default settings and modifying existing code
of applications.
Inferring Complex Inplace Model Transformation Rules
Timo Kehrer (HU Berlin) Optimal support for continuous evolution in
modelbased software development requires tool environments to
be customisable to domainspecific modelling languages
(DSMLs). An important aspect are the set of change operations
available to modify models. Inplace model transformations
have shown to be wellsuited to define model refactorings and
other kinds of complex change operations. However, the
specification of transformation rules requires a deep
understanding of the language metamodel, limiting it to
expert tool developers and language designers. This is at odds
with the aim of domainspecific visual modelling environments,
which should be customisable by domain experts. This
talk reports about ongoing research mitigating this problem,
following a model transformation byexample 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, multiobject
patterns and global invariants.
PrivacybyDesign Framework for Internet of Things
Charith Perera (Open University) The Internet of Things (IoT) systems are
designed and developed either as standalone applications from
the groundup 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 privacybydesign 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) Smart contracts are selfenforcing 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 nonstandard 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, OpinionDiffusion, and Liquid Democracy
Davide Grossi (University of Liverpool) 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).
RequirementsDriven Mediation for Collaborative Security
Amel Bennaceur (Open University) 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, toolsupported approach for
collaborative security based on a combination of feature
modelling and mediator synthesis. I will show how we used the
FICS (Featuredriven 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) 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) (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 modelbased recursive partitioning which can bridge the theory and datadriven 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) Ada, Countess of Lovelace (18151852) 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) (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 2025 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/worldeconomicforumgovernmentsblockchain
2. https://www.cryptocoinsnews.com/theuktreasuryisembracingblockchaindigitalcurrenciesandbigdataresearch
3. http://uk.businessinsider.com/santanderhas2025usecasesforbitcoinsblockchaintechnologyeverydaybanking20156
4. http://tallysticks.io/
5. http://www.forbes.com/sites/valleyvoices/2015/12/21/whytheblockchainisthenewwebsite/#2715e4857a0b742d9a29ac2e
6. Blockchain.open.ac.uk
Semester 2, 2015/16Seminar programme
Seminar details
Letterio Galletta (Pisa) 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 IoTLySa
is presented which is endowed with constructs to model this
kind of system. Furthermore, IoTLySa 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)
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 discretetime stochastic modelling analysis of a congestion control mechanism for Internet traffic and a new approach for constraining endtoend delay to a specified value. The feasibility of the system is examined using theoretical analysis, simulation and testbed.
Differentially Private Policy Evaluation
Borja De Balle Pigem (Lancaster) 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)
Quantum Structure and the Mathematical Modeling of Human Decision Making
Sandro Sozzo (Leicester) 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 underextension
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
nonclassical phenomena has led to the development of
quantumbased 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 quantumtheoretic
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
quantumtheoretic 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 LargeScale Graph Processing
Eiko Yoneki (Cambridge) 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, largescale computing
environment. I would introduce our recent work on the graph
processing that have billionscale 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) 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 sessiontyped π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
sessionlike 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 datadriven, complex networks view of computational search spaces
Gabriela Ochoa (Stirling) 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 (HeriotWatt) Nominal techniques take variable symbols as firstclass entities in the mathematical foundations  so the variable symbol "x" is a firstclass primitive datum; and is not represented by e.g. a functional argument or a number. (Technically, "x" is an urelement in FraenkelMostowski 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 theoremproving, 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):
* Firstorder logic.
* The lambdacalculus.
* Quine's NF.
Using these models I have amongst other things given Stone duality constructions for firstorder logic and the untyped lambdacalculus (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.
AlignmentFree Sequence Comparison: Using Positive and Negative Information
Solon Pissis (King's College London) 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 alignmentfree techniques, which are based on measures
referring to the composition of sequences in terms of their
constituent patterns. These measures, such as qgram 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 qgrams 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 lineartime and linearspace 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 spatiotemporal model checking
Vincenzo Ciancia (Pisa) Socalled 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 spatialtemporal logics. We also
discuss some ongoing applications of spatiotemporal model
checking to analysis of bike sharing systems, medical imaging
and computational linguistics.
Helen Petrie (York) Evaluation of user experience (UX) in
crosscultural 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
crosscultural UX research. A localized websurvey was
designed and data collected from 92 respondents in two
cultures, Nigeria and AngloCeltic (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) 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 ultralargescale. In this briefing, we discuss the privacy challenges posed by such an ultralargescale 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) 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
nonsecure) 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) 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/16Seminar programme
Seminar details
Frank Wolter (University of Liverpool) Ontologybased 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 nontractable. In this talk,
I will first introduce ontologybased 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 nonuniform approaches to
understanding the complexity of query answering in
ontologybased data access for expressive ontology
languages.
Geographic Information and Information Geographies
Stefano De Sabbata (University of Leicester) 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) Traditionally, countries viewed international
border control as mostly immigration and customsbased
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 skillsets. 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 intelligenceled 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 kbarrier coverage in a
given belt region? Given an appropriate network density, how
to determine if a region is indeed kbarrier 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) 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.
Levelbased Analysis of Evolutionary Algorithms under Uncertainty
Per Kristian Lehre (University of Nottingham) Evolutionary algorithms have been applied for
decades to tackle hard, realworld optimisation problems in
logistics, the automotive industry, the pharmaceutical
industry, and elsewhere. Despite their widespread use, the
theoretical understanding of evolutionary algorithms is still
relatively poorly developed. Partly due to lack of methods,
timecomplexity 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
timecomplexity analysis of evolutionary algorithms, the
levelbased 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. Levelbased 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 levelbased method, we investigate how
evolutionary algorithms cope under different forms of
uncertainty in pseudoBoolean 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) 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 machinecomprehensible 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)
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 icecream)
Danica Vukadinovic Greetham (University of Reading) 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) 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/15Seminar programme
Seminar detailsSome mathematical aspects of data centre networks
Iain Stewart (Durham) 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, faulttolerance
and throughput. Consequently, these initial designs, though
often impressive, tend to be prototypical with the intention
being to demonstrate proofofconcept 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) 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 automatabased decision procedure for PA
with modulo counting quantifiers has the same
tripleexponential 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) 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) 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.
MultiLinear Algebraic Semantics for Natural Language
Mehrnoosh Sadrzadeh (Queen Mary) 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, noncategorical
models.
Diagrammatic mathematics and signal flow graphs
Pawel Sobocinski (Southampton) 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
stringdiagrammatic theory of boolean circuits, we discovered
the theory of Interacting Hopf Algebras. As well as being
closely related to Coecke and Duncan's ZXcalculus 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, whichin contrast to the primary role
traditionally given to themturn 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 EconomicsDriven Perspective
Rami Bahsoon (University of Birmingham) The
architecture of the system is the first design artifact that
realizes the nonfunctional requirements of the system such as
security, reliability, availability, modifiability, realtime
performance and their tradeoffs. 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
nonfunctional 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 nonfunctional requirements, while
continuing to add value. We motivate the need for an
economicsdriven 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) 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.
Signal processing helping cure cardiac arrhythmias Fernando Schlindwein (Bioengineering Research Group, University of Leicester) 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 realtime 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)
(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/15Seminar programme
Seminar detailsFrom Communicating Machines to Graphical Choreographies
Julien Lange
(Imperial College London) Graphical
choreographies, or global graphs, are general multiparty
session specifications featuring expressive constructs such as
forking, merging, and joining for representing
applicationlevel 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 finitestate 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)
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
nondeterminism 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 Maudebased 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) Today's enterprises demand a high degree of
compliance of business processes to meet regulations, such as
SarbanesOxley 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 designtime aspects of
compliance management and secondarily on business process
runtime monitoring; hence, providing preventive lifetime
compliance support. While current manual or adhoc 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 designtime and the reasoning
and analysis of detected compliance violations.
Massimo Bartoletti (University of Cagliari) 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
communicationcorrect. 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
communicationcorrectness results can be obtained, e.g. that
the application is deadlockfree. 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 contractoriented
calculus CO2. In particular, we show how to safely
overapproximate the honesty property by a modelchecking
technique which abstracts from the contexts a service may be
engaged with.
Logical Foundations for SessionBased Concurrency: Overview and Recent Developments
Jorge Perez (Groningen, The Netherlands) (based on joint works with Luis Caires, Frank
Pfenning, and Bernardo Toninho) A central concept in the theory
of programming languages is the socalled CurryHoward
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 propositionsastypes/proofsasprograms correspondence, in
the style of the CurryHoward isomorphism, but in the context
of concurrent processes defined in the picalculus. 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 domainaware setting, relying
on a linear logic augmented with "worlds" from hybrid logic,
here interpreted as distributed locations (or sites).
Encodings of Range MaximumSum Segment Queries and Applications
Pat Nicholson (MPI Saarbruecken) Given an array A containing arbitrary (positive
and negative) numbers, we consider the problem of supporting
range maximumsum 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 maximumsum 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 kcovers: 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)
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 speedup over competing stateoftheart approaches.
This is joint work with S. Kiefer, J. Ouaknine, B. Wachter and J. Worrell.
Anders Bruun (Aalborg University)
The concept of User Experience (UX) in HumanComputer
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 stateofthe 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)
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
peerreview 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) 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
ShinIchi Minato (Hokkaido University, Japan) In many scientific communities using experiment
databases, one of the crucial problems is how to assess the
statistical significance (pvalue) of a discovered
hypothesis. Especially, combinatorial hypothesis assessment is
a hard problem because it requires a multipletesting
procedure with a very large factor of the pvalue
correction. Recently, Terada et al. proposed a novel method of
the pvalue correction, called "Limitless Arity
Multipletesting 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 pvalue correction than previous method, and it
empowers the scientific discovery. However, the original LAMP
implementation is sometimes too timeconsuming 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 pvalue patterns in quite short time even for very
largescale databases.


Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356. 