ABOUT 
Computer Science SeminarsUseful links:
Semester 2, 2014/15Seminar programme
Seminar detailsInteger 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. 