Computer Science Seminars
Stefan Kahrs (University of Kent)
Search trees are a commonly used data structure to implement sets or finite maps. To prevent degenerate scenarios one normally uses a variant of search trees with a built-in mechanism to keep them in balance. Best known of these are AVL trees and red-black trees, of which the latter are cheaper to maintain whilst they stay not quite as well in balance as the former. Inspired by differences between iterative and recursive versions of red-black trees, we are attempting to create a hybrid that tries to combine the better aspects of both. The hybrid's approach to tree maintenance could be described as "lazy" - though effectively it is merely working with a different invariant. Interestingly, the mechanism still operates well with a yet weaker invariant, in which the trees are used for the majority of the time as ordinary search trees, i.e. without maintenance overhead.
Justin Ward (University of Warwick)
In the standard, unweighted set packing problem, we are given a collection of sets of elements and must find the largest possible sub-collection of sets such that no element occurs in more than one set. In this talk, I will consider a restriction of the set packing problem in which all of the given sets contain at most k elements, for some constant k. This restricted setting, which is called k-set packing, captures a wide variety of allocation and optimization problems, and is in fact NP-hard for k > 2. One simple algorithmic approach to the k-set packing problem is local search. The standard local search algorithm maintains a current collection of disjoint sets and repeatedly tries to enlarge this collection by adding some small number of new sets to the collection and removing the sets that share elements with these sets. The algorithm terminates when no such small change improves the current collection. Despite its relative simplicity, this approach (or variants thereof) is the state of the art for k-set packing problems. In this talk, I will present current algorithmic results for both the unweighted and weighted variants of k-set packing, as well as the monotone submodular variant, in which the value of a group of sets satisfies the natural economic property of diminishing returns. I will discuss some known performance barriers for local search algorithms in each of these settings. Then, I will show how novel modifications of the standard technique can be used to move past these barriers, giving algorithms that return solutions of higher a guaranteed value than standard local search algorithms. Although the results are stated (and hold) in the theoretical setting of worst-case analysis, this talk will focus primarily on general algorithmic design principles that may also be employed in a variety of practical settings.
Torkil Clemmensen (Copenhagen Business School)
In this talk, I present an emerging framework for human work interaction design (HWID), and explore a case of designing a simple folder structure for a new e-learning software program for a university study program. The aim is to contribute to the theoretical base for human work interaction design (HWID) by identifying the type of relations connecting design artifacts with work analysis and interaction design processes. I present a piece of research in which the action research method was used, with me in a double role as university researcher and project manager of a developer group within the university. The analysis was conducted through grounded theory, inspired by the HWID framework. I outline how the findings support the use of a holistic framework with asymmetrical relations between work analysis and design artifacts, and between design artifacts and interaction design. In conclusion, I give suggestions for modifying the general framework, and recommendations for a HWID approach to design artifacts. The talk is intended to inspire discussion about how to connect empirical work analysis and interaction design activities.
Janet Read (University of Central Lancashire)
This talk will put participatory design of interactive technology with children under scrutiny. I will examine the practices of the author, and others, around the inclusion of children in participatory design activities and will highlight some of the concerns that are often skimmed over in the literature. An example PD activity which resulted in technologies being provided for a school in Uganda will be used as a backdrop to the discussion. The talk will be well suited to anyone interested in the ethical involvement of children in research, in anyone interested in cross cultural design and will also be relevant to those considering user based research and / or development in a range of contexts.
Mariangiola Dezani (Universitą di Torino)
The subtyping systems of mobile processes have been extensively studied since early 1990s as one of the most applicable concepts in the types for concurrency. Their correctness has been usually provided as the soundness of subtyping relations with respect to the type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the greatest subtyping relation possible without violating type safety, solely based on operational semantics. This talk discusses a technique for formalising and proving that a subtyping system is precise (i.e. both sound and complete) with respect to the type safety in the pi-calculus, and applies it to synchronous and asynchronous session calculi. The well-known session subtyping, the branching-selection subtyping, turns out to be sound and complete in the synchronous calculus. Instead in the asynchronous calculus, this common subtyping is incomplete with respect to the type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T is not a subtype of S. We then propose an asynchronous subtyping system which is sound and complete with respect to the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtyping systems with respect to desired safety properties.
Phil Trinder (SCIEnce Team, HPC-GAP Team, Glasgow University)
The talk describes interdisciplinary work between Computer Science and Mathematics. We start by outlining Computer Algebra Systems (CAS), an important class of Mathematical software. We describe the design and implementation of a new way of combining CAS, the Symbolic Computation Software Composability Protocol (SCSCP). We show how SCSCP-compliant components may be combined to solve scientific problems that cannot be solved within a single system, or may offer mathematical software services. The SCSCP Protocol has become a de facto standard for mathematical software with implementations available for 7 CAS, and libraries for C/C++ and Java. We sketch the challenges posed by large-scale algebraic computations, and outline the SymGrid-Par architecture designed to address these challenges. We report performance results showing that SymGrid-Par delivers performance comparable with bespoke parallel CAS, copes with high levels of irregular parallelism, can generate new Mathematical results, and can provide performance portability. We briefly outline the design of SymGrid-Par2, a scalable, reliable successor to SymGrid-Par, and report good performance on an 1800 core architecture. The work is supported by both the EU Framework Programme and the EPSRC.
Andrew Fish (University of Brighton)
The EPSRC funded project Automatic Diagram Generation aims to build a unified framework for the automatic generation of mixed-type diagrams arising as the integration of Euler diagrams, knot diagrams, and graphs. The intent is to bring theoretical benefits via methods which make use of commonality of abstraction, together with practical-oriented benefits in terms of generic tool support for areas such as diagrammatic logics, or ontology and network visualisations. The talk will primarily discuss a new encoding for Euler diagrams, adapting the notion of Gauss Paragraphs for knot diagrams, providing a richer abstraction than has been previously considered, encapsulating the structure of the diagram, whilst also providing generation machinery. We provide a further connection between knots and Euler diagrams via the construction of rewriting methods which, for example, yield a family of Brunnian links which project to Edwards' construction of Venn diagrams. The talk should be accessible, containing examples demonstrating the underlying algorithmic procedures. A live demo of the associated software, which integrates theories about knots and Euler diagrams, whist utilising existing graph drawing libraries, may even be provided.
Katya Komendantskaya (University of Dundee)
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal mathematical proofs and verification of hardware and software systems. These frameworks usually involve thousands of definitions and theorems (for instance, there are approximately 4200 definitions and 15000 theorems in the formalisation of the Feit-Thompson theorem; and more than 5000 theorems in the formalisation of a C compiler). The size of the libraries, as well as their technical and notational sophistication often stand on the way of efficient knowledge re-use. Very often, it is easier to start a new library from scratch rather than search the existing proof libraries for potentially common heuristics and techniques. The main question we address in this talk is: Can statistical pattern recognition help in creation of more convenient and user-friendly proof environments, in which statistically significant proof patterns could be used as proof-hints? We will survey the most successful state-of-the art machine-learning tools for theorem proving, and will present the tool ML4PG (“Machine-Learning for Proof General”) – an Emacs-based interface that allows Coq/SSReflect users to find interesting proof patterns interactively during the proof-development. We will show how ML4PG works for mathematical and industrial libraries. ML4PG tool is the main outcome of the EPSRC First Grant “Machine-Learning Automated Proofs”. The webpage of ML4PG with downloadable software and papers can be found here.
Thorsten Altenkirch (University of Nottingham)
I have recently spend a semester at the Institute of Advanced Study in Princeton to attend a special year on ”Homotopy Type Theory” (HoTT) and participated in creating the HoTT book which is freely available on the internet. In my talk I will give you my own account why I think that HoTT is interesting especially for Computer Science, I will give you a taste of HoTT and also tell you what are the missing pieces of the puzzle.
Igor Razgon (Birkbeck College London)
Behzad Bordbar (University of Birmingham)
The Cloud is intended to handle large amounts of data. In addition, to benefit from the economies of scale, the applications and Operating Systems are homogenized to a few images restricting the variations of products used within the Cloud. As a result, vulnerability can be exploited on a large number of machines and the attacker can be sure of a high pay-off for their activities. This makes the Cloud a prime target for malicious activities. There is a clear need to develop automated, adaptive and computationally-inexpensive methods of discovering malicious behaviour as soon as they start such that remedial actions can be adopted before substantial damage is done. In this seminar, we will describe a method of detecting malware by identifying the symptoms of malicious behaviour as opposed to looking for the malware itself. This can be compared to the use of symptoms in human pathology, in which study of symptoms direct physicians to diagnosis of a disease or possible causes of illnesses. The main advantage of shifting the attention to the symptoms is that a wide range of malicious behaviour can result in the same set of symptoms. We will also describe our current implementation of the proposed approach with the help of very small Virtual Machines (VM) that can monitor other VMs to discover the symptoms. FVMs collaborate with each other in identifying symptoms by exchanging messages via secure channels. The FVMs report to a Command and Control module that collects and correlates the information so that suitable remedial actions can take place in real-time. The Command and Control can be compared to the physician who infers possibility of an illness from the occurring symptoms. A sketch of our current implementation which involves using Mini-OS on the Xen virtualisation platform will also be presented. This research is in collaboration with Cloud and Security lab at HP.
Roberto Micalizio (Universitą degli Studi di Torino)
Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356.