Computer Science Seminars
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 IoT-LySa is presented which is endowed with constructs to model this kind of system. Furthermore, IoT-LySa is equipped with a static analysis able to approximate the behaviour of the system and to predict how data gathered from sensors spread and are manipulated inside the network. We also discuss how this output of this analysis can be used to verify some security properties of IoT system.
Lin Guan (Loughborough University)
With the rapid development of the Internet, Quality of Service (QoS) has become one of the most important issues in present networks, especially enabling different types of traffic to satisfy specified QoS constraints. This talk will present discrete-time stochastic modelling analysis of a congestion control mechanism for Internet traffic and a new approach for constraining end-to-end delay to a specified value. The feasibility of the system is examined using theoretical analysis, simulation and test-bed.
Borja De Balle Pigem (Lancaster)
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)
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 under-extension in concept combinations, revealed that classical theories, e.g., (fuzzy set) logic and Kolmogorovian probability theory, are structurally incompatible with a possible model for the collected experimental data. Similarly, classical structures were shown to be incompatible with human decision making (prisoner’s dilemma, disjunction effect, conjunction fallacy) and behavioural economics (Ellsberg and Machina paradoxes). The seek of a satisfactory explanation of these non-classical phenomena has led to the development of quantum-based models. Interestingly, quantum models have provided a simple but powerful way to cope with these effects, faithfully modeling empirical data. And more, they have been consistently verified and extended to more complex situations, thus leasing to the configuration of a growing research community, called quantum cognition. We illustrate here some interesting results we have obtained within our quantum cognition research, with an emphasis on the formalization and representation of natural concepts and their combinations in terms of quantum structures. We firstly show that the data collected on combinations of two concepts cannot generally be modeled in a classical (Kolmogorovian) probability space. Successively, we present a general quantum-theoretic framework that allows faithful modeling of different collections of experimental data on conjunctions, disjunctions and negations of two concepts, including a recent one performed by ourselves. This perspective describes, at the same time, the observed deviations from classical (fuzzy set) logic and probability theory in terms of quantum probability and genuine quantum effects (contextuality, emergence, entanglement and interference). Starting from our successful quantum-theoretic framework, we then formulate a unifying explanatory hypothesis for the above mentioned experimental findings. In it, human reasoning is the superposition of two processes – a conceptual reasoning, whose nature is emergence of new conceptuality, and a logical reasoning, founded on an algebraic calculus of the logical type. We provide arguments to maintain that the former reasoning prevails over the latter in most cognitive processes. Hence, the originally observed experimental deviations from classical logical reasoning should not be interpreted as biases of human mind but, rather, as natural expressions of emergence in its deepest form. Inspired by this quantum cognition research, we finally illustrate the basics of a quantum meaning based framework for information retrieval (IR) and natural language processing (NLP). The potential advantages of this approach with respect to traditional approaches, such as latent semantic analysis (LSA), are also briefly discussed.
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, large-scale computing environment. I would introduce our recent work on the graph processing that have billion-scale of vertices and edges in a commodity single computer, which requires secondary storage as external memory. Executing algorithms results in access to such secondary storage and performance of I/O takes an important role, regardless of the algorithmic complexity or runtime efficiency of the actual algorithm in use.
Dominic Orchard (Imperial College London)
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the λ-calculus and its variants, the latter for the π-calculus. In this talk, I explore their relative expressive power. I'll first give some background for those unfamiliar with either effect systems or session types. Then, I show an embedding from PCF, augmented with a parameterised effect system, into a session-typed π-calculus (session calculus), showing that session types are powerful enough to express effects with linear continuation behaviour. Secondly, I give a reverse embedding, from the session calculus back into PCF , by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. This is joint work with Nobuko Yoshida, presented at POPL ’16.
Gabriela Ochoa (Stirling)
Computational search is fundamental for solving optimisation problems arising in industry, science and society. A variety of search algorithms have been proposed, but little attention has been devoted to understanding the structure of search spaces. This talk starts by introducing computational search and optimisation using the famous travelling salesman problem as a case study. It then overviews a new model of computational search spaces based on complex networks. Search spaces can be analysed and visualised as complex networks, revealing intriguing structures that shed new light into why some problems are harder to solve than others.
Jamie Gabbay (Heriot-Watt)
Nominal techniques take variable symbols as first-class entities in the mathematical foundations --- so the variable symbol "x" is a first-class primitive datum; and is not represented by e.g. a functional argument or a number. (Technically, "x" is an urelement in Fraenkel-Mostowski set theory.) It turns out that astonishing richnesses of structure emerge which have been applied: first in the semantics of inductively defined abstract syntax, and then in theorem-proving, concurrency, rewriting, automata theory, and much more. In recent work I have been applying these ideas to the foundation of mathematics itself. Specifically, I've studied models of three systems in nominal algebra (algebra enriched with names) and nominal powersets (sets of sets enriched with names): * First-order logic. * The lambda-calculus. * Quine's NF. Using these models I have amongst other things given Stone duality constructions for first-order logic and the untyped lambda-calculus (an open problem), and also a claimed proof of the open problem of the consistency of Quine's NF. These results are interesting in themselves, they have philosophical significance, and it is clear that the methods used in the proofs are general and interesting, and that the further possibilities are probably extensive. I will endeavour to deliver an accessible --- that's right: accessible, to the best of my ability! --- guided tour of this material. Technical familiarity will not be required to have a good time. Courageous or reckless readers can access relevant papers here: www.gabbay.org.uk/papers.html#semooc, www.gabbay.org.uk/papers.html#repdul, www.gabbay.org.uk/papers.html#conqnf.
Solon Pissis (King's College London)
Sequence comparison is a prerequisite to virtually all comparative genomic analyses. It is often realized by sequence alignment techniques, which are computationally expensive. This has led to increased research into alignment-free techniques, which are based on measures referring to the composition of sequences in terms of their constituent patterns. These measures, such as q-gram distance, are usually computed in time linear with respect to the length of the sequences. In this talk, we visit two recent results: (a) we introduce a new distance measure based on q-grams and show how it can be applied effectively and computed efficiently for circular sequence comparison [WABI 2015]; (b) we focus on the complementary idea: how two sequences can be efficiently compared based on information that does not occur in the sequences. A word is an absent word of some sequence if it does not occur in the sequence. An absent word is minimal if all its proper factors occur in the sequence. We present the first linear-time and linear-space algorithm to compare two sequences by considering all their minimal absent words. In the process, we present results of combinatorial interest, and also extend the proposed techniques to compare circular sequences [LATIN 2016].
Vincenzo Ciancia (Pisa)
So-called spatial logics are a family of logical languages in which some connectives are interpreted according to the characteristics of a mathematical structure representing space. Such languages are aimed at describing properties of points or regions by how they are spatially related to each other. Even though, in principle, spatial reasoning could be applied to several domains, and a plethora of potential practical applications easily come to the mind, so far very few attempts were made in putting such ideas into practice. In this talk, we discuss recent work in implementing spatial reasoning in the form of the model checker “topochecker” for spatial and spatial-temporal logics. We also discuss some ongoing applications of spatio-temporal model checking to analysis of bike sharing systems, medical imaging and computational linguistics.
Helen Petrie (York)
Evaluation of user experience (UX) in cross-cultural settings is vital for the development of interactive systems due to the globalization of markets and the search for good user experience in interactive systems. Although interactive systems are distributed globally, users are always local and this should be taken into consideration in methods and materials used in the cross-cultural UX research. A localized web-survey was designed and data collected from 92 respondents in two cultures, Nigeria and Anglo-Celtic (AC) countries (Australia, Canada, Ireland, and the UK). We found that Nigerian respondents are more positive in their ratings than AC respondents, irrespective of content, and are less likely to criticize in their feedback. The culture of the respondents and culture of the visual materials of the scenarios does matter in respondents’ reactions, but the way it matters is not straightforward, and there are complex interactions. We expected that our results would show a strong identification with one’s own cultural group, but this turns out to be only one aspect of a scenario that may affect respondents’ reactions. Therefore care needs to be taken in localizing visual materials and in interpreting the results from different cultural groups.
Pauline Anthonysamy (Google)
There will be an estimated 35 zettabytes (35×10^21) of digital records worldwide by the year 2020. This effectively amounts to privacy management on an ultra-large-scale. In this briefing, we discuss the privacy challenges posed by such an ultralarge-scale ecosystem - we term this “Privacy in the Large”. We will contrast existing approaches to privacy management, reflect on their strengths and limitations in this regard and outline key software engineering research and practice challenges to be addressed in the future.
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 non-secure) OSs (e.g. Android). For this reason, a security issue in the hypervisor can compromise the security of the complete system. We present our experience in applying formal verification of information flow security for a simple hypervisor for ARMv7. The verification is done by combining interactive theorem proving with analysis tools for binary code.
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.
Frank Wolter (University of Liverpool)
Ontology-based data access is concerned with querying incomplete data sources in the presence of domain specific knowledge provided by an ontology. A central problem in this setting is that for many classes of ontology and query languages query answering becomes non-tractable. In this talk, I will first introduce ontology-based data access and its applications. Then I will give an overview of weak languages for which query answering is tractable and of the most important techniques for answering queries in this case. Finally, I will discuss non-uniform approaches to understanding the complexity of query answering in ontology-based data access for expressive ontology languages.
Stefano De Sabbata (University of Leicester)
Information has always had geography. It is from somewhere; about somewhere; it evolves and is transformed somewhere. The first part of the talk will be concerned with the place where geography meets information retrieval and mobile information services. What is special about the spatial component of the data that describe our world, that we store, map, and retrieve? What criteria do we have to take into account when searching for geographic information and how to assess the geographic relevance of information? The second part of the talk will focus on the different geographies of information, and in particular on the geographies of the internet. What factors influence internet access, and how does this reflect on content production? Where does internet content come from, which places are more or less represented, and how does this matter?
Mohammad Hammoudeh (Manchester Metropolitan University)
Traditionally, countries viewed international border control as mostly immigration- and customs-based challenge. However, with the increased risks of terrorism, illegal movement of drugs, weapons, contraband and people, these countries face unprecedented challenges in securing borders effectively. Securing international borders is a complex task that involves international collaboration, deployment of advanced technological solutions and professional skill-sets. In the current financial climate, governments strive to secure their borders, but also ensure that costs are kept low. Wireless Sensor Networks (WSNs) is a low cost technology that can provide an effective solution to the range of problems faced in securing borders effectively. The ability of a WSN to operate without human involvement and in situations where other surveillance technologies are impractical has made it favourite for deployment in hostile hazardous environments. This technology offers intelligence-led approach to strengthen vulnerable points on the international borders. This class of WSN applications imposes a linear network topology, which has nodes daisy chained using radio communication. Linear WSN topologies are characterised by sparse node deployment, long data transmission distances and alignment of nodes along a virtual line. This talk presents solutions to address the new challenges introduced by Linear WSNs, including: What is the minimum network density to achieve k-barrier coverage in a given belt region? Given an appropriate network density, how to determine if a region is indeed k-barrier covered? How to find a path connecting the two ends of the border such that every point on the path is covered by a sensor node? How to balance workload across sensor nodes? How to elongate network life time and meet quality of service requirements?
Ian Horrocks (University of Oxford)
So called "Semantic Technologies" are rapidly becoming mainstream technologies, with RDF and OWL now being deployed in diverse application domains, and with major technology vendors starting to augment their existing systems accordingly. This is, however, only the first step for Semantic Web research; we need to demonstrate that the Semantic Technologies we are developing can (be made to) exhibit robust scalability if deployments in large scale applications are to be successful. In this talk I will review the evolution of Semantic Technologies to date, and show how research ideas from logic based knowledge representation developed into a mainstream technology. I will then go on to examine the scalability challenges arising from deployment in large scale applications, and discuss ongoing research aimed at addressing them.
Per Kristian Lehre (University of Nottingham)
Evolutionary algorithms have been applied for decades to tackle hard, real-world optimisation problems in logistics, the automotive industry, the pharmaceutical industry, and elsewhere. Despite their wide-spread use, the theoretical understanding of evolutionary algorithms is still relatively poorly developed. Partly due to lack of methods, time-complexity analysis of evolutionary algorithms have mainly focused on simple algorithms, such as the (1+1) EA which do not use a population or sophisticated genetic operators. This talk introduces a new method for time-complexity analysis of evolutionary algorithms, the level-based method (Corus et al, PPSN'2014). This method provides upper bounds on the expected hitting times of a wide class of stochastic population models from easy to verify conditions. Level-based analysis has already been applied to study complex algorithms, such as genetic algorithms using crossover, and estimation of distribution algorithms. As an application of the level-based method, we investigate how evolutionary algorithms cope under different forms of uncertainty in pseudo-Boolean optimisation. We first consider the classical additive noise model, where the objective function is perturbed by a noise term. Secondly, we consider partial evaluation, in which only a random subset of the terms in the objective function are evaluated. The analysis shows that with appropriate settings of mutation rate, selective pressure, and population size, an evolutionary algorithm can cope with surprisingly high levels of uncertainty.
Marija Slavkovik (University of Bergen)
Machine ethics is an emerging discipline in artificial intelligence research that is concerned with ensuring that the behaviour of machines towards humans and other machines they interact with is ethical. The idea of machine ethics has tickled the fancy of numerous science fictions writers and aficionados, but as of recently, the advancements in robotics and automated systems have shaped this idea into a research topic. Any machine ethics has to be based on human understanding of morality. What kind of autonomous systems should be enhanced with ethical reasoning capabilities? What are the main approaches and challenges to transform vague ideas of right and wrong into machine-comprehensible specifications? Once you get autonomous machines to behave ethically, how can you make sure that they will? How does machine ethics impact other facets of society, or, when a machine misbehaves who is to blame? This talk will explain these questions and the ongoing research efforts towards answering them.
Alistair Edwards (University of York)
The way people speak tells a lot about their origins – geographical and social, but when someone can only speak with the aid of an artificial voice (such as Stephen Hawking), conventional expectations are subverted. This seminar will explore some of the limitations and possibilities of speech technology.
Danica Vukadinovic Greetham (University of Reading)
In this talk, I will look at the problem of centrality ranking in dynamic networks. Centrality is an intuitive concept that tells us how important or involved an individual node is in a network. Many different definitions exist, but not all will work in evolving networks where edges are created and destroyed in each time step. We focus here on one that works well, slightly modified, in evolving networks, Katz centrality, and show how it can be calculated efficiently for relatively large networks.
We then use this calculation to inform a decision on a network based intervention and report the results from several small scale human studies where we observed (and interfered with) the mood dynamics on evolving communication networks.
This is a joint work with Zhivko Stoyanov from Reading and Peter Grindrod from Oxford University.
Kirsten Barrett (Department of Geography)
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.
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, fault-tolerance and throughput. Consequently, these initial designs, though often impressive, tend to be prototypical with the intention being to demonstrate proof-of-concept and practical viability rather than to detail the finished article. Not only does improving and optimizing data centre networks provide opportunities for theoreticians to delve into their mathematical toolboxes but particular aspects of data centre network design can also lead to new problems that perhaps might not be immediately practically relevant but are interesting in their own right from a theoretical perspective. In this talk I shall introduce some of the practical considerations behind data centre network design and show how different aspects of mathematics impinge on this world; such aspects might include isoperimetric sets within graphs, the utilization of combinatorial design theory and the reduction of core data centre problems to combinatorics.
Dietrich Kuske (TU Ilmenau)
We consider Presburger arithmetic (PA) extended with modulo counting quantifiers. We show that its complexity is essentially the same as that of PA, i.e., we give a doubly exponential space bound. This is done by giving and analysing a quantifier elimination procedure similar to Reddy and Loveland's procedure for PA. Furthermore, we show that the complexity of the automata-based decision procedure for PA with modulo counting quantifiers has the same triple-exponential complexity as the one for PA when using least significant bit first encoding. (joint work with Peter Habermehl, LIAFA)
Jonathan Hayman (Cambridge)
Causal reasoning is a powerful tool in analysing security protocols, as seen in the popularity of the strand space model. However, for protocols that branch, more subtle models are needed to capture the ways in which protocols can interact with a possibly malign environment, for example allowing the expression of security properties of the form ``no matter what the attacker does, the protocol can still achieve a particular goal''. We study a model for security protocols encompassing causal reasoning and interaction, developing a semantics for a simple security protocol language based on concurrent games played on event structures. We show how it supports causal reasoning about a protocol for secure digital signature exchange. The semantics paves the way for the application of more sophisticated forms of concurrent game, for example including symmetry and probability, to the analysis of security protocols.
Alessandro Abate (Oxford)
This talk looks at the development of abstraction techniques based on quantitative approximations, in order to investigate the dynamics of complex systems and to provide computable approaches for the synthesis of control architectures. The approach employs techniques and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on stochastic hybrid systems, which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear). A case study in energy networks, dealing with the problem of demand response, is employed to clarify concepts and techniques.
Mehrnoosh Sadrzadeh (Queen Mary)
Vector spaces offer a contextual way of reasoning about word meanings and have been rather successfully applied to natural language processing tasks. But the basic contextuality hypothesis of these models does not quite work when it comes to phrases and sentences. Herein, one needs to apply Frege's principle of Compositionality and use operations on word vectors to combine them. The high level categorical models of vector spaces (inspired by the work of Abramsky and Coecke on quantum models) have provided a general such setting for compositionality of contextual models. In this talk, I will present this model (joint work with Clark and Coecke), go over a number of its concrete instantiations, and present experimental results on language tasks (joint work with Grefenstette and Kartsaklis). The latter have outperformed the results of the simple, non-categorical models.
Pawel Sobocinski (Southampton)
In recent years there have been a number of developments in the area of symmetric monoidal theories (SMTs), a generalisation of algebraic theories in which one considers operations of arbitrary arity and coarity together with equations, and in which linearity is default: variables cannot be copied and discarded. String diagrams are an intuitive and powerful graphical syntax for the terms of SMTs. I will report on recent joint work with Filippo Bonchi and Fabio Zanasi, in which, building on the work of Steve Lack on composing SMTs via distributive laws and Yves Lafont on a string-diagrammatic theory of boolean circuits, we discovered the theory of Interacting Hopf Algebras. As well as being closely related to Coecke and Duncan's ZX-calculus for quantum circuits, the associated string diagrams amount to a rigorous and intuitive diagrammatic universe for linear algebra: familiar concepts such as linear transformations and linear spaces appear as certain string diagrams. As well as giving a new way to look at classical topics in linear algebra, string diagrams sometimes carry useful computational information. I will show how a special case of the theory of Interacting Hopf Algebras captures signal flow graphs, which are a classical circuit notation for linear dynamical systems. When signal flow graphs are considered as string diagrams, diagrammatic reasoning gives a novel, sound and complete technique to reason about them. I will explain how the underlying mathematics leads us to reconsider some popular assumptions about the roles of causality and direction of signal flow, which---in contrast to the primary role traditionally given to them---turn out to be secondary, derived notions: in this way, this work connects with recent trends in control theory, in particular the Behavioural Approach, popularised by Jan Willems.
Rami Bahsoon (University of Birmingham)
The architecture of the system is the first design artifact that realizes the non-functional requirements of the system such as security, reliability, availability, modifiability, real-time performance and their trade-offs. We discuss the challenges in managing change and guiding evolution in large scale software architecture, where uncertainty and dynamism are the norm. We report on ongoing work on evaluating software architectures for sustainability. We posit that the linkage between architectural design decisions, evolution trends of non-functional requirements and sustainability should be explicit; such linkage can provide insights on the success (failure) of software evolution. We argue that one of major indicators of architecture sustainability is the extent to which the architecture design decisions can endure evolutionary changes in non-functional requirements, while continuing to add value. We motivate the need for an economics-driven approach based on the principles of Real Options for valuing software architecture for sustainability. The objective is to assist the architect in strategic “what if” analysis for sustainability involving valuing the flexibility of the architecture to change and/or valuing the worthiness of designing or reengineering for change.
Stephane Ducasse (INRIA)
In this presentation I will argue for the need of dedicated tools and present the approach developed around Moose (http://www.moosetechnology.org) and engineered in Synectique (http://www.synectique.eu) a spinoff of the RMOD group. I will present some industrial cases and the meta tools that we have such as Roassal, Glamour.
Fernando Schlindwein (Bioengineering Research Group, University of Leicester)
Atrial Fibrillation is the most common cardiac arrhythmia. Patients with AF are five times more likely to have a stroke. We are going to show how using real-time signal processing can help cure AF using catheter ablation of the areas responsible for the generation or maintenance of AF.
Michel Chaudron (Chalmers)
(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.
(Imperial College London)
Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In this talk, I will present (i) an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and (ii) a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed.
Alberto Lluch Lafuente (Technical University of Denmark)
Memory consistency is sometimes given up for the sake of performance both in concurrent and in distributed systems. Operational models of consistency relaxations like relaxed memory models offer suitable abstractions that can be used for various purposes (e.g. verification) but pose some challenges in state space exploration activities (e.g. verification) in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make the analysis of programs under relaxed consistency feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar state space exploration purposes.
Amal Elgammal (Trinity College Dublin)
Today's enterprises demand a high degree of compliance of business processes to meet regulations, such as Sarbanes-Oxley and Basel III. To ensure continuous guaranteed compliance, it should be enforced during all phases of the business process lifecycle, from the phases of analysis and design to deployment, monitoring and adaptation. This course of research primarily concentrates on design-time aspects of compliance management and secondarily on business process runtime monitoring; hence, providing preventive lifetime compliance support. While current manual or ad-hoc solutions provide limited assurances that business processes adhere to relevant constraints, there is still a lack of an established generic framework for managing these constraints; integrating their relationships and maintaining their traceability to sources and processes; and automatically verifying their satisfiability. In this talk, I will present my research results that address the problems of automating the compliance verification activities during design-time and the reasoning and analysis of detected compliance violations.
Massimo Bartoletti (University of Cagliari)
Distributed applications can be constructed by composing services which interact by exchanging messages according to some global communication pattern, called choreography. Under the assumption that each service adheres to its role in the choreography, the overall application is communication-correct. However, in wild scenarios like the Web or cloud environments, services may be deployed by different participants, which may be mutually distrusting (and possibly malicious). In these cases, one can not assume (nor enforce) that services always adhere to their roles. Many formal techniques focus on verifying the adherence between services and choreographic roles, under the assumption that no participant is malicious; in this case, strong communication-correctness results can be obtained, e.g. that the application is deadlock-free. However, in wild scenarios such techniques can not be applied. In this talk we present a paradigm for designing distributed applications in wild scenarios. Services use contracts to advertise their intended communication behaviour, and interact via sessions once a contractual agreement has been found. In this setting, the goal of a designer is to realise honest services, which respect their contracts in all execution contexts (also in those where other participants are malicious). A key issue is that the honesty property is undecidable in general. In this talk we discuss veriﬁcation techniques for honesty, targeted at agents specified in the contract-oriented calculus CO2. In particular, we show how to safely over-approximate the honesty property by a model-checking technique which abstracts from the contexts a service may be engaged with.
Jorge Perez (Groningen, The Netherlands)
(based on joint works with Luis Caires, Frank Pfenning, and Bernardo Toninho) A central concept in the theory of programming languages is the so-called Curry-Howard isomorphism: it tightly relates, on the one hand, logical propositions and types; on the other hand, it connects proofs and functional programs. This isomorphism has proved essential to endow reasoning techniques over sequential programs with clean principles, which have both operational and logical meanings. In 2010, Caires and Pfenning put forward an interpretation of linear logic propositions as session types for communicating processes. Remarkably, this result defines a propositions-as-types/proofs-as-programs correspondence, in the style of the Curry-Howard isomorphism, but in the context of concurrent processes defined in the pi-calculus. In this talk, I will give an overview to Caires and Pfenning's interpretation, from the perspective of languages for concurrency. I will also present some associated developments, which complement the interpretation by Caires and Pfenning: logical relations, typed behavioral equivalences, and type isomorphisms. If time permits, I will discuss two further developments. The first concerns the analysis of choreographies (multiparty protocols defined by session types) using the type discipline induced by Caires and Pfenning's interpretation. The second result extends the Caires and Pfenning's interpretation to a domain-aware setting, relying on a linear logic augmented with "worlds" from hybrid logic, here interpreted as distributed locations (or sites).
Pat Nicholson (MPI Saarbruecken)
Given an array A containing arbitrary (positive and negative) numbers, we consider the problem of supporting range maximum-sum segment queries on A: i.e., given an arbitrary range [i,j], return the subrange [i' ,j' ] ⊆ [i,j] such that the sum of the numbers in A[i'..j'] is maximized. Chen and Chao [Disc. App. Math. 2007] presented a data structure for this problem that occupies Θ(n) words, can be constructed in Θ(n) time, and supports queries in Θ(1) time. Our first result is that if only the indices [i',j'] are desired (rather than the maximum sum achieved in that subrange), then it is possible to reduce the space to Θ(n) bits, regardless the numbers stored in A, while retaining the same construction and query time. We also improve the best known space lower bound for any data structure that supports range maximum-sum segment queries from n bits to 1.89113n bits. Finally, we provide a new application of this data structure which simplifies a previously known linear time algorithm for finding k-covers: i.e., given an array A of n numbers and a number k, find k disjoint subranges [i_1 ,j_1 ],...,[i_k ,j_k ], such that the total sum of all the numbers in the subranges is maximized.
Andrzej Murawski (University of Warwick)
We present APEX, a tool for analysing probabilistic programs that are open, i.e. where variables or even functions can be left unspecified. APEX transforms a program into an automaton that captures the program’s probabilistic behaviour under all instantiations of the unspecified components. The translation is compositional and effectively leverages state reduction techniques. APEX can then further analyse the produced automata; in particular, it can check two automata for equivalence which translates to equivalence of the corresponding programs under all environments. In this way, APEX can verify a broad range of anonymity and termination properties of randomised protocols and other open programs, sometimes with an exponential speed-up over competing state-of-the-art approaches. This is joint work with S. Kiefer, J. Ouaknine, B. Wachter and J. Worrell.
Anders Bruun (Aalborg University)
The concept of User Experience (UX) in Human-Computer Interaction has evolved over the past 10 years. UX is typically considered to cover a broad range of dimension going beyond usability of interactive products. This talk will firstly provide a brief overview of state-of-the art in UX research. Secondly, the talk will present results from a recent experiment questioning the reliability of current practices for assessing UX. UX is typically measured retrospectively through subjective questionnaire ratings, yet we know little of how well these retrospective ratings reflect concurrent experiences of an entire interaction sequence. The talk will present findings from an empirical study of the gap between concurrent and retrospective ratings of UX. Alternative methods of assessing UX will be discussed, which have considerable implications for practice.
Jun Zhao (Lancaster University)
Scientific integrity is facing growing scrutiny. We read more and more high profile stories about scientific ‘flaws’ and embarrassment, which not only have serious impact on the life of generations but also that of the scientists themselves. All of these have recently led to serious doubts about the significance of the results and quality of the peer-review process, with peer review costing an estimated $2 billion US dollars each year. Provenance information records where a data item came from and how it was produced. A driving theme in provenance research is to understand how best to use provenance as the critical evidence to support scientists justifying and validating their findings and improve the efficiency and efficacy of the peer review process. In this talk, I will discuss the role of provenance research in enhancing reproducibility of computational research and examine the critical gap in existing provenance research for fulfilling this goal. I will outline our approach of applying semantic web technologies to provenance data mining and argue an important role to be played by data mining technologies in provenance data analytics at a large scale.
Cecilia Mascolo (University of Cambridge)
In this talk I will describe our research in the area of mobile sensing and mobile phone sensing. I will introduce a variety of projects which we have conducted to monitor people’s mobility and behaviour with handheld devices as well as embedded technology. I will introduce the challenges related to mobile sensing and the solutions which we have proposed in terms of power preservation and behaviour inference. The specific studies described include Emotion Sense, a platform to monitor mood and behaviour for psychological studies, our work on using location and accelerometer data to understand parking and driving patterns and a study using RFID technology to monitor interaction and use of space in buildings.
Shin-Ichi Minato (Hokkaido University, Japan)
In many scientific communities using experiment databases, one of the crucial problems is how to assess the statistical significance (p-value) of a discovered hypothesis. Especially, combinatorial hypothesis assessment is a hard problem because it requires a multiple-testing procedure with a very large factor of the p-value correction. Recently, Terada et al. proposed a novel method of the p-value correction, called "Limitless Arity Multiple-testing Procedure" (LAMP), which is based on frequent itemset enumeration to exclude meaninglessly infrequent itemsets which will never be significant. The LAMP makes much more accurate p-value correction than previous method, and it empowers the scientific discovery. However, the original LAMP implementation is sometimes too time-consuming for practical databases. We propose a new LAMP algorithm that essentially executes itemset mining algorithm once, while the previous one executes many times. Our experimental results show that the proposed method is much (10 to 100 times) faster than the original LAMP. This algorithm enables us to discover significant p-value patterns in quite short time even for very large-scale databases.
Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356.