ABOUT 
Computer Science SeminarsUseful links:
Semester 2, 2015/16Seminar programme
Seminar detailsQuantum 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. 