Device drivers are a major cause of OS crashes and hangs. As drivers spend much of their time handling queues of requests, and these requests are stored as mutable linked lists, many of these errors come from not maintaining a memory safety invariant. SLAyer is a program analysis tool designed to prove the absence of memory safety errors such as dangling pointer references and double frees. Towards this goal, SLAyer searches for invariants that form proofs in Separation Logic. Complex composite data structures like cyclic doubly linked-lists are supported using parametrized recursive predicates. SLAyer is aimed at moderately sized (10-30K) systems-level code bases written in C; it is fully automatic and does not require annotations or hints from the programmer.

Biography

Samin Ishtiaq is Principal RSDE in the Programming Principles and Tools group at Microsoft Research Cambridge. He works on the SLAyer (Separation Logic-based memory safety for C programs), TERMINATOR (program termination) and BioCheck (analysis of gene regulatory networks) projects. Samin joined MSR in April 2008. Before that, he worked at ARM, where he did CPU modeling and verification to help tape-out the Cortex A8, Cortex M3 and SC300 processors, and the AMBA bus protocol checker. Samin has an MEng from Imperial and a PhD in dependent type theory from Queen Mary. He was an RA on the original Verified Bytecode project.

Paterson lecture

Nick Jennings, Southampton University

Computational Service Economies: Design and Applications

Thursday, January 26th 2012. 4pm, CS1.01

Abstract

Many modern computing systems have to operate in environments that are highly interconnected, highly unpredictable, without a central control authority, and in which the constituent components are owned by a variety of stakeholders that each have their own aims and objectives. Relevant exemplars include the Web, the Smart Electricity Grid, Peer-to-Peer systems, Pervasive Computing and many eCommerce applications. Now, I believe that all of these systems can operate under the same fundamental conceptual model: (i) entities offer a variety of services in some form of institutional setting; (ii) other entities connect to these services (covering issues such as service discovery, service composition and service procurement); and (iii) entities enact services in a flexible and context sensitive manner. Moreover, I believe agent-based computing is an appropriate computational model for such systems. In particular, autonomous agents are a natural way of viewing flexible service providers and consumers and the interactions between these autonomous components are naturally modeled as some form of economic trading process that, if successful, results in a transaction between the agents involved.

In this talk, the focus will be on the methods and techniques for designing the electronic institutions and the interaction strategies of the participants. In so doing, I will touch upon techniques from the areas of game theory, coalition formation, automated negotiation and computational mechanism design. Relevant exemplars of applications built using such techniques in the domains of sensor networks, autonomous systems, smart grids, and disaster response will also be discussed.

Biography

Professor Jennings divides his time between his posts as a Chief Scientific Advisor to the UK Government and Professor of Computer Science in the School of Electronics and Computer Science at Southampton University, where he heads the Agents, Interaction and Complexity Group (he previously headed the Intelligence, Agents, Multimedia Group). He is also the Chief Scientist for aroxo and lostwax/aerogility.

Nick is an internationally-recognised authority in the areas of agent-based computing and intelligent systems. His research covers both the science and the engineering of such systems. Specifically, he has undertaken fundamental research on automated bargaining, auctions, markets, mechanism design, trust and reputation, coalition formation and decentralised control. He has also pioneered the application of multi-agent technology; developing some of the first real-world systems (in domains such as business process management, energy systems, sensor networks, disaster response, telecommunications, and eDefence) and generally advocating the area of agent-oriented software engineering.

In undertaking this research, he has attracted grant income of over £20M (mainly from EPSRC), published more than 500 articles (with some 250 co-authors) and graduated 30 PhD students (two of whom have won the BCS/CPHC Distinguished Dissertation Award). He is recognised as highly cited by ISI Web of Science in both the Engineering and the Computer Science categories. With over 40,000 citations in Google Scholar, he is the second most highly cited researcher in the area of artificial intelligence (according to Microsoft's Academic Search system) and has an h-index of 86 (the second top non-American according to Palsberg). He has received a number of international awards for his research: the Computers and Thought Award (the premier award for a young AI scientist and the first European-based recipient in the Award's 30 year history), the ACM Autonomous Agents Research Award and an IEE Achievement Medal. He is a Fellow of the Royal Academy of Engineering, the Institute of Electrical and Electronic Engineers, the British Computer Society, the Institution of Engineering and Technology (formerly the IEE), the Association for the Advancement of Artificial Intelligence (AAAI), the Society for the Study of Artificial Intelligence and Simulation of Behaviour (AISB), and the European Artificial Intelligence Association (ECCAI) and a member of Academia Europaea and the UK Computing Research Committee (UKCRC).

Nick was the founding Editor-in-Chief of the International Journal of Autonomous Agents and Multi-Agent Systems, is a member of the scientific advisory board of the German AI Institute (DFKI) and a founding director of the International Foundation for Autonomous Agents and Multi-Agent Systems. He has also led teams that have won competitions in the areas of: the Iterated Prisoners' Dilemma (the 20th Anniversary competitions in 2004 and 2005), RoboCup Rescue (the Infrastructure competition in 2007), Agent Trust and Reputation (the ART competitions in 2006 and 2007), the Lemonade Stand Game (2009 & 2010), and Market Design (the TAC CAT competition in 2007).

The daily software engineering life - How to be prepared

Thursday, January 12th 2012. 4pm, CS1.01

Abstract

How is life as a real software engineer, out there in the wild? This talk gives an overview of today's software engineering in practice. We talk about what it means to build and ship software in various kinds of companies, ranging from modern and flexible ones like Google or Facebook to more traditional ones like large insurance companies, for example. We discuss the most important challenges people are facing when implementing, testing, shipping and supporting software systems, the role of soft-skills in this area, why you need to understand the domain you are building software for, and what it means to ship new versions of a software several times a day. We talk about the role of agile software development methods and how they changed the landscape, why they are an essential part of today's software engineering - and what people should better have learned at University before jumping onto this playground.

Biography

Martin works at VMware, where he leads the tooling development team - the team that is responsible for the Spring IDE, the SpringSource Tool Suite and the Cloud Foundry Integration for Eclipse. His work is focused on building development tools, working with the community, and creating a flexible, modern and agile development process with his team. Before joining VMware Martin founded it-agile GmbH, one of the leading agile consulting companies in Germany, where he worked with teams across Germany and Europe on agile software development, flexible and modular architectures and Eclipse technologies. He is committer for various open-source projects, author of a number of articles about agile software development, and co-author of several books. He is also a frequent speaker at non-academc software engineering conferences. Martin got a Diploma in Informatics from the University of Hamburg in 1999, with a focus on software engineering and object-orientation.

Richard Dearden, University of Birmingham

Model-based fault diagnosis for an autonomous underwater vehicle

Thursday, December 1st 2011. 4pm, CS1.01

Abstract

In this talk I describe work on the automatic fault diagnosis of an autonomous underwater vehicle (AUV), using a model-based approach. I will describe Livingstone 2, a discrete fault diagnosis system that has been deployed in a number of applications including spacecraft, and how this was used to diagnose Autosub 6000, a research AUV operated by the National Oceanography Centre. I will also look at some of the difficulties encountered in applying such a discrete approach, and describe recent research on hybrid diagnosis for the domain using algorithms built around a satisfiability modulo theory solver.

Biography

Dr. Richard Dearden has been a Senior Lecturer in the School of Computer Science at the University of Birmingham since 2005. He works in the broad area of reasoning under uncertainty, and in particular on planning, execution, and fault diagnosis, all applied to autonomous robots. Before that he spent 5 years leading the Model-based Diagnosis and Recovery group at NASA Ames Research Centre where he worked primarily on Mars rover diagnosis and planning. His Ph.D. (2000) was in Markov decision process planning at the University of British Columbia.

Jose Fiadeiro, University of Leicester

A Formal Approach to Service-Oriented Modelling

Thursday, November 24th 2011. 4pm, CS1.01

Abstract

This talk provides an overview of a formal approach that we have developed within the FP6-IST-FET Integrated Project SENSORIA (www.sensoria-ist.eu [www.sensoria-ist.eu]), which aimed at providing formal support for modelling service-oriented systems in a way that is independent of the languages in which services are programmed and the platforms over which they run. We discuss the semantic primitives that are provided in the SENSORIA Reference Modelling Language (SRML) for modelling composite services, ie. services who business logic involves a number of interactions among more elementary service components as well the invocation of services provided by external parties. This includes a logic for specifying stateful, conversational interactions, a language and semantic model for the orchestration of such interactions, and an algebraic framework supporting service discovery, selection and dynamic assembly.

Biography

I did my undergraduate degree in Mathematics at the University of Lisbon (Faculty of Science), after which I moved to the Technical University of Lisbon (Department of Mathematics, Faculty of Engineering) where I studied for a PhD under the supervision of Amilcar Sernadas. I was awarded my doctorate in 1989, and then spent three years doing research at Imperial College London with a grant from the European Commission. I became Associate Professor in Computer Science at the Technical University of Lisbon in 1992, and moved to the University of Lisbon (Department of Informatics, Faculty of Science) in 1993. Before I joined Leicester in 2002, I held visiting research positions at Imperial College, King’s College London, PUC-Rio de Janeiro, and the SRI International. I was Head of Department at Leicester between August 2006 and July 2011.

My current research interests are in formal aspects of software system modelling and analysis in the context of global ubiquitous computing. I am a member of the Steering Committees of WS-FM (Workshop on Web Services and Formal Methods), CALCO (Conference on Algebra and Coalgebra in Computer Science, which I co-founded with Jan Rutten) and WADT (Workshop on Algebraic Development Techniques). I was chairman of the IFIP WG 1.3 (Foundations of System Specification) in 2004-09, and chairman of the Steering Committee of ETAPS (European Joint Conferences on Theory and Practice) in 2002-04. I am also member of the Editorial Board of Information Processing Letters (Elsevier).

Jon Timmis, University of York

From Immune Systems to Robots

Thursday, November 10th 2011. 4pm, CS1.01

Abstract

There are many areas of bio-inspired computing, where inspiration is taken from a biological system to construct an engineered solution. This talk will focus on the use of the immune system and its application to anomaly detection of chemical spectra in a robotic sniffer dog and to self-healing swarm robotic systems. In the first case, we will explore work undertaken with Dstl where we are attempting to develop an automated improvised explosive device (IED) detection system. For this work, we have abstracted signalling mechanisms from T cells, an important cell in an immune response. In the second study, one of self-healing swarm systems, we explore how we have exploited an immune response known as granuloma formation, to create a swarm that is capable to deciding how best to cope with energy failure scenarios. We will also explore the pitfalls of a bio-inspired approach and illustrate how computational modelling of immune systems can aid in bio-inspird algorithm design.

Biography

Jon Timmis is Professor of Natural Computation at the University of York and holds a joint appointment between the Department of Electronics and the Department of Computer Science. His primary research is in the area of computational immunology and bio-inspired fault tolerance in embedded systems, with a focus on swarm robotic systems. He gained his PhD in Computer Science from the University of Wales, Aberystwyth. He holds a senior Royal Society Research fellowship, a Wolfson Research Merit Award, to investigate the development of self-healing swarm robotic systems.

Jean-Christophe Olivo-Marin, Institut Pasteur

Cells, images and numbers

Thursday, October 20th 2011. 4pm, CS1.01

Abstract

I will present specific methods and algorithms for the processing and quantification of 2- and 3-D+t images sequences in biological microscopy and demonstrate algorithms of PSF approximations for image deconvolution, image segmentation, multi-particle tracking and active contours models for cell shape and deformation analysis. One specific goal in biological imaging is indeed to automate the quantification of dynamics parameters or the characterization of phenotypic and morphological changes occurring as a consequence of cell/cell or pathogens/host cells interactions. The availability of this information and its thorough analysis is of key importance to help deciphering the underlying molecular mechanisms. I will illustrate our methods in projects related to the study of the dynamics of genes in cell nuclei, the movement of parasites in cells and the detection and tracking of microbes in cells.

Biography

J.-C. Olivo-Marin, PhD, is the head of the Quantitative Image Analysis Unit at the Institut Pasteur. He was a co-founder and Chief Technology Officer of the Institut Pasteur Korea, Seoul. He has a long experience of multi-disciplinary approaches in biological imaging, and his research interests are in image analysis of multidimensional microscopy images, pattern recognition and motion analysis for cellular dynamics studies. He is a member of the Bio Imaging and Signal Processing Technical Committee (BISP-TC) of the IEEE Signal Processing Society.

Ton Coolen, King's College London

Counting and generating tailored random graphs

Thursday, October 13th 2011. 4pm, CS1.01

Abstract

Ensembles of tailored random graphs with controlled topological properties are a natural and rigorous language for describing biological networks. They suggest precise definitions of structural features, allow us to classify networks and obtain precise (dis)similarity measures, provide `null models' for hypothesis testing, and can serve as efficient proxies for real networks in process modelling. Mathematically and computationally, the key questions are (i) how to calculate the Shannon entropy of tailored random graphs analytically (giving the effective number of graphs with given imposed topological features) and (ii) how to generate such graphs numerically, with any specified probability distribution. Surprisingly, most algorithms used in the past for generating complex graphs are biased, rendering many studies on biological networks meaningless. We show how both problems can be solved exactly, using information-theoretic and statistical mechanical tools.

Biography

Coolen obtained his PhD in theoretical physics from the University of Utrecht; he came to the Oxford in 1991, and joined King's College London in 1995. He is a member of the Advisory Panel of Journal of Physics A, the BBSRC Systems Biology Board, and a Fellow of the London Institute for Mathematical Sciences. He has published two books, more than 130 refereed papers, and supervised 17 PhD students; for details see http://www.mth.kcl.ac.uk/~tcoolen. Coolen specialises in the mathematical analysis of large heterogeneous many-variable systems in physics, biology, computer science, and economics, statistical mechanics and stochastic processes, Bayesian and information-theoretic analysis, and the theory of complex networks. In recent years he has focused his research mainly on problems in bio-medicine. He created and led for many years the Disordered Systems group in Mathematics at King's College, and is now setting up an Institute for Mathematical and Molecular Biomedicine at King's, see http://www.mth.kcl.ac.uk/IMMB, which aims to become a leading centre for the development of advanced mathematical and computational methods for modern biomedicine.

Paulo Mateus, SQIG - Instituto de Telecomunicações Lisbon

Minimizing probabilistic and quantum automata

Monday, September 26th 2011. 2pm, CS1.01

Abstract

Quantum gadgets are becoming available in the market, namely for communicating over optical fiber. The major engineering problem concerning such gadgets is the size of quantum memory that can be entangled. While it is more or less trivial to generate two entangled qubits, it is still science fiction to entangle much more than ten qubits. When working with such restrictions, a basic question occurs: what is the minimal number of (entangled) qubits required to perform a certain task? This question is equivalent to an open problem posed by Moore and Cruchfield in 2000 concerning the decidability of minimizing quantum automata. Furthermore, this question is already connected with another open problem from 1979, by Paz, concerning the existence of a Myhill-Nerode minimization algorithm for stochastic machines/probabilistic automata. We show that both these problems are decidable, and that there exists an EXPSPACE minimization algorithm for both quantum and probabilistic automata. Joint work with D. Qiu.

Biography

Born in 1975 in Lisbon, studied at IST where he got his PhD in 2001 with a thesis on the interconnection of probabilistic systems. In the Fall semester of 2001-02, he was a postdoc at the Logic and Computation Group, Department of Mathematics, University of Pennsylvania. In 2006, he obtained his agregação (habilitation) in Mathematics from the Technical University of Lisbon. His habilitation thesis was awarded the Portuguese IBM Scientific Prize 2005. Currently, he is an Associate Professor at the Department of Mathematics of IST and coordinates the Security and Quantum Information Group at Instituto de Telecomunicações.

Leslie Valiant, Harvard University

Holographic Algorithms

Tuesday, July 12th 2011. 4pm, MS.05

Abstract

Using the notion of polynomial time reduction computer scientists have discovered an astonishingly rich web of interrelationships among the myriad computational problems that arise in diverse applications. These relationships can be used both to give evidence of intractability, such as that of NP-completeness, as well as to provide efficient algorithms.

In this talk we discuss a notion of a holographic reduction that is more general than the traditional one in the following sense. Instead of locally mapping solutions one-to-one, it maps them many-to-many but preserves some measure such as the sum of the solutions. One application is to finding new polynomial time algorithms where none was known before. Another is to give evidence of intractability. There are pairs of related problems that can be contrasted in this manner. For example, for a skeletal version of Cook's 3CNF problem (restricted to be planar and where every variable occurs twice positively) the problem of counting the solutions modulo 2 is NP-hard, but counting them modulo 7 is polynomial time computable. Holographic methods have proved useful in establishing dichotomy theorems, which offer a more systematic format for distinguishing the easy from the probably hard. Such theorems state that for certain wide classes of problems every member is either polynomial time computable, or complete in some class conjectured to contain intractable problems.

Biography

Leslie Valiant was educated at King's College, Cambridge; Imperial College, London; and at Warwick University where he received his Ph.D. in computer science in 1974. He is currently T. Jefferson Coolidge Professor of Computer Science and Applied Mathematics in the School of Engineering and Applied Sciences at Harvard University, where he has taught since 1982. Before coming to Harvard he had taught at Carnegie Mellon University, Leeds University, and the University of Edinburgh.

His work has ranged over several areas of theoretical computer science, particularly complexity theory, computational learning, and parallel computation. He also has interests in computational neuroscience, evolution and artificial intelligence.

He received the Nevanlinna Prize at the International Congress of Mathematicians in 1986, the Knuth Award in 1997, the European Association for Theoretical Computer Science EATCS Award in 2008, and the 2010 A. M. Turing Award. He is a Fellow of the Royal Society (London) and a member of the National Academy of Sciences (USA).

Mark Josephs, WMG Digital Laboratory

Processes through the Looking Glass: Reflections on an Algebra for Delay-Insensitive Circuits [slides]

Thursday, May 26th 2011. 4pm, CS1.04

Abstract

In his 1988 Turing Award Lecture, Ivan Sutherland advocated the transition-signalling conceptual framework as it "offers the opportunity to build up complex VLSI systems by hierarchical composition from simpler pieces". The approach has its origins in the Macromodular Computer Design project at Washington University, St. Louis (1965-1974). In 1989, I started to collaborate with some Dutch researchers who had been developing its theoretical foundations and this collaboration quickly led to an algebraic approach (based on Hoare's Communicating Sequential Processes) to the design of delay-insensitive (DI) circuits. In this talk I shall give a short introduction to our so-called DI-Algebra, before focussing on more recent results based on the idea of constructing the mirror or reflection of a process.

Reference: M.B. Josephs and H.K. Kapoor (2007) Controllable Delay-Insensitive Processes, Fundamenta Informaticae 78(1):101-130
URL: http://inf.lsbu.ac.uk/ccsv/josephmb/PreprintOfFundamInfVol78No1pp101-130.pdf

Biography

Mark Josephs joined the University of Warwick in 2010. He received his BSc in Mathematics from University College, London, and his MSc and DPhil in Computation from the University of Oxford. He is an Honorary Professor of London South Bank University, a Chartered Fellow of the BCS, and a Senior Member of the IEEE. His memberships also include the Editorial Board of the Computer Journal, the EPSRC Peer Review College, and the UK Computing Research Committee.

Tony Tan, University of Edinburgh

Algorithms for static analysis in web databases

Thursday, May 19th 2011. 4pm, CS1.04

Abstract

The web has brought fundamentally new challenges to data management. The key features that distinguish web data from traditional database applications are its structure: usually described by mark-up languages, such as XML.

The simplest abstraction of XML documents is ordered unranked finite trees whose nodes are labeled by letters from a finite alphabet. This abstraction works well for reasoning about structural properties, but real XML documents carry data, which cannot be captured by a finite alphabet. Thus, there has been a consistent interest in data trees, i.e., trees in which nodes carry both a label from a finite alphabet and a data value from an infinite domain. It seems natural to add at least the equality on data values to a logic over data trees. But while for finitely-labeled trees many logical formalisms -- such as monadic second-order logic -- are decidable; adding data-equality makes even first-order logic undecidable. This explains why the search for decidable reasoning formalisms over data trees has been a common theme in XML research.

In this talk I will give a brief survey on results and techniques that have been developed in the research of data trees and data words. Some of the results have surprisingly deep connections with other well known models of computation such as vector addiction systems and automata with Presburger constraints.

Biography

Tony Tan is currently a postdoc (under Leonid Libkin) in the School of Informatics, University of Edinburgh. He got his B.Sc and M.Sc. in National University of Singapore in 2003 and 2005, respectively, and PhD in Technion in 2009.

Nasir Memon, Polytechnic Institute of New York University

Photo Forensics - There is more to a picture than meets the eye

Thursday, May 12th 2011. 11am, CS0.07 (provisional)

Abstract

Given an image or a video clip can you tell which camera it was taken from? Can you tell if it was manipulated? Given a camera or even a picture, can you find from the Internet all other pictures taken from the same camera? Forensics professionals all over the world are increasingly encountering such questions. Given the ease by which digital images can be created, altered, and manipulated with no obvious traces, digital image forensics has emerged as a research field with important implications for ensuring digital image credibility. This talk will provide an overview of recent developments in the field, focusing on three problems. First, collecting image evidence and reconstructing them from fragments, with or without missing pieces. This involves sophisticated file carving technology. Second, attributing the image to a source, be it a camera, a scanner, or a graphically generated picture. The process entails associating the image with a class of sources with common characteristics (device model) or matching the image to an individual source device, for example a specific camera. Third, attesting to the integrity of image data. This involves image forgery detection to determine whether an image has undergone modification or processing after being initially captured.

Biography

Nasir Memon is a Professor in the computer science department at the Polytechnic Institute of New York University, New York. He is the director of the Information Systems and Internet Security (ISIS) lab at Polytechnic (http://isis.poly.edu). Prof. Memon received his BE in Chemical Engineering and MS in Math from BITS, Pilani, India, 1981. He received his MS in Computer Science (1989) and PhD in Computer Science (1992) from the University of Nebraska, Lincoln.

Prof. Memon's research interests include Digital Forensics, Data Compression, Computer and Network Security and Multimedia Computing and Security. He has published more than 250 articles in journals and conference proceedings and holds 6 patents in image compression and security with six more pending application. He has won several awards including the NSF CAREER award and the Jacobs Excellence in Education award. His research has been featured in NBC nightly news, NY Times, MIT Review, Wired.Com, New Science Magazine etc.

He is currently the Editor-in-Chief of the IEEE Transactions on Information Security and Forensics. He was an associate editor for IEEE Transactions on Image Processing, the Journal of Electronic Imaging, the ACM Multimedia Systems Journal, the LNCS Transaction on Data Hiding, IEEE Security and Privacy Magazine, IEEE Signal Processing Magazine and the International Journal on Network Security. Prof. Memon is the co-founder of Digital Assembly (http://www.digital-assembly.com) and Vivic Networks (http://www.vivic.com), two early stage start-ups in NYU-Poly's incubator. He is a fellow of the IEEE and an IEEE Signal Processing Society distinguished lecturer for the years 2011 and 2012.

Shum Prakash (Warwick Ventures) and Olivia Johansson (Venner Shipley LLP)

IP protection and the commercialisation of algorithms and software

Thursday, May 12th 2011. 4pm, CS1.04

Biography

Dr Shum Prakash, Business Development Manager, Warwick Ventures, Technology Transfer Office (Tel: 024 7657 4145; Email: s.prakash@warwick.ac.uk). After her BSc in Chemistry (Wales), Shum read for her PhD in Biochemistry (Kent) and undertook R&D with Nihon Medi-Physics Co. Ltd and Johnson Matthey Plc to develop radiopharmaceutical drugs for cancer therapy and brain diagnosis. After her MSc in Science and Technology Policy (Sussex), Shum was a consultant at SQW Ltd providing feasibility studies, evaluations and recommendations to many organisations supporting science and technology. She joined Warwick Ventures in December 2001 as a Business Development Manager where she has taken a broad range of technologies from concept to royalty generating commercial licenses and to trading spin off companies. Whilst at Warwick, Shum completed her MBA (Warwick) for which she was awarded a Sainsbury Management Fellowship. She is also a panel member for the RISC fund managed by the NIHR, Department of Health.

Olivia Johansson is a Chartered and European patent Attorney, specialising in electronics, physics and computer implemented inventions at Venner Shipley LLP. Olivia has particular experience in the field of telecommunications and consumer electronics, as well as in satellite technology. Before becoming a patent attorney she worked for a number of university spin-out companies where she developed software. She has particular interest in the fast changing fields of computer memory, processing power and software. Her clients include both multi-national corporations and small start-up companies.

Paul Goldberg, University of Liverpool

The Complexity of the Homotopy Method, Equilibrium Selection, and Lemke-Howson Solutions

Thursday, May 5th 2011. 4pm, CS1.04

Abstract

Homotopy methods envisage the following general approach to finding a Nash equilibrium of a game. Consider a version of the game where the payoffs have been modified so that there is some obvious Nash equilibrium. Then, continuously change those numbers back towards the values in the game of interest, keeping track of how the Nash equilibrium changes (it should change continuously). The Lemke-Howson algorithm is a very well-known algorithm that can be expressed as a homotopy method.

In the talk, we will see the surprising result that the Lemke-Howson solutions (as well the outputs of other homotopy methods) are PSPACE-complete to compute. This is somewhat paradoxical since the Lemke-Howson method performs very well in practice. This result ties in with earlier work relating the complexity of games, to the complexity class PPAD. But, I will keep the talk reasonably self-contained.

Biography

Paul Goldberg is a professor at the department of Computer Science at Liverpool, and head of the Economics and Computation research group. He was previously at the University of Warwick (1997-2006), and before that, at Sandia National Labs (USA) and Aston University. His research currently focuses on equilibrium computation, and models of decentralised interaction of agents.

Martyn Amos, Manchester Metropolitan University

An early warning method for crush

Thursday, March 17th 2011. 4pm, CS1.04

Abstract

Fatal crush conditions occur in crowds with tragic frequency. Event organizers and architects are often criticised for failing to consider the causes and implications of crush, but the reality is that the prediction and mitigation of such conditions offers a significant technical challenge. Full treatment of physical force within crowd simulations is precise but computationally expensive; the more common method of human interpretation of results is computationally "cheap" but subjective and time-consuming. In this talk we describe an alternative method for the analysis of crowd behaviour, which uses information theory to measure crowd disorder. We show how this technique may be easily incorporated into an existing simulation framework, and validate it against an historical event. Our results show that this method offers an effective and efficient route towards automatic detection of crush.

(Joint work with Peter Harding).

Biography

Martyn Amos is a Reader in the School of Computing, Mathematics and Digital Technology at Manchester Metropolitan University, and the Head of the Novel Computation Group. He received his B.Sc. in Computer Science from Coventry University (1993) and his Ph.D. in DNA computing from the University of Warwick (1997). He then held a Leverhulme Special Research Fellowship (University of Liverpool), before permanent academic positions at the Universities of Liverpool (1999-2002) and Exeter (2002-2006). He is currently the Principal Investigator of three projects; the European Commission FP7-funded BACTOCOM (Bacterial Computing) and COBRA (Coordination of Biological and Chemical-IT Research Activities) projects, and the EPSRC-supported Bridging the Gaps: NanoInfoBio project. He has an active interest in public engagement with science, and is the author of the popular science book "Genesis Machines: The New Science of Biocomputing".

Rob Cross, Centre for Mechanochemical Cell Biology, Warwick Medical School

Engines of self organization: mechanochemical cell biology of kinesins and microtubules

Thursday, March 10th 2011. 4pm, CS1.04

Abstract

Increasing evidence suggests that molecular motors not only pull, push and move along their microtubule tracks, but also modify the assembly dynamics of the micortubule polymers. This creates a potential for patterns of cytoskeletal trafficking to feed back on the structure of the network. My colleagues and I are interested in this and are studying as a model system the regulated dynamics of microtubules in a model cell, the fission yeast S. pombe, using high resolution TIRF and dark field microscopy. Mal3 is an EB-family protein that bintracks the tips of polymerising microtubules and drives towards the A-lattice arrangement of protofilaments, in contrast to the more usual B-lattice. Alp14 and Dis1 are related TOG-family proteins in S. pombe that we find act catalytically to accelerate microtubule growth by up to 10-fold. Klp5 and Klp6 are kinesin-8 family motors whose properties allow them to detect the arrival of microtubule tips at cell ends, and to specifically promote catastrophic depolymerisation of microtubules arriving at cell ends. Our current computational activities are largely in image processing, but we are increasingly interested in developing realistic simulations of complex, dynamic motor-track systems.

Biography

Rob Cross is a biophysical cell biologist who works on the mechanisms of bio-molecular motors and the polymerisation dynamics of their tracks. He is professor and director of the newly-established centre for mechanochemical cell biology at Warwick medical school. Rob and his colleagues use techniques in structural biology, transient kinetics, advanced optical microscopy, protein engineering and molecular cell biology to try to understand the machinery of motor-driven spatiotemporal self-organization in biology.

Ingemar Cox, University College London

Probably Approximately Correct Search

Thursday, March 3rd 2011. 4pm, CS1.04

Abstract

We consider the problem of searching a document collection using a set of independent computers. That is, the computers do not cooperate with one another either (i) to acquire their local index of documents or (ii) during the retrieval of a document. During the acquisition phase, each computer is assumed to randomly sample a subset of the entire collection. During retrieval, the query is issued to a random subset of computers, each of which returns its results to the query-issuer, who consolidates the results. We examine how the number of computers, and the fraction of the collection that each computer indexes, affects performance in comparison to a traditional deterministic configuration. We provide analytic formulae that, given the number of computers and the fraction of the collection each computer indexes, provide the probability of an approximately correct search, where a "correct search'' is defined to be the result of a deterministic search on the entire collection. We show that the randomized distributed search algorithm can have acceptable performance under a range of parameters settings. Simulation results confirm our analysis.

Biography

Ingemar J. Cox is currently Professor and Director of Research in the Department of Computer Science at University College London. He is Head of the Future Media Group at UCL.

He has been a recipient of a Royal Society Wolfson Fellowship (2002-2007). He received his B.Sc. from University College London and Ph.D. from Oxford University. He was a member of the Technical Staff at AT&T Bell Labs at Murray Hill from 1984 until 1989 where his research interests were focused on mobile robots. In 1989 he joined NEC Research Institute in Princeton, NJ as a senior research scientist in the computer science division. At NEC, his research shifted to problems in computer vision and he was responsible for creating the computer vision group at NECI. He has worked on problems to do with stereo and motion correspondence and multimedia issues of image database retrieval and watermarking. In 1999, he was awarded the IEEE Signal Processing Society Best Paper Award (Image and Multidimensional Signal Processing Area) for a paper he co-authored on watermarking. From 1997-1999, he served as Chief Technical Officer of Signafy, Inc, a subsidiary of NEC responsible for the commercialization of watermarking. Between 1996 and 1999, he led the design of NEC's watermarking proposal for DVD video disks and later colloborated with IBM in developing the technology behind the joint "Galaxy" proposal supported by Hitachi, IBM, NEC, Pioneer and Sony. In 1999, he returned to NEC Research Institute as a Research Fellow.

He is a Fellow of the IEEE, the IET (formerly IEE), and the British Computer Society. He is a member of the UK Computing Research Committee. He was founding co-editor in chief of the IEE Proc. on Information Security and is an associate editor of the IEEE Trans. on Information Forensics and Security. He is co-author of a book entitled "Digital Watermarking" and its second edition "Digital Watermarking and Steganography", and the co-editor of two books, "Autonomous Robots Vehicles" and "Partitioning Data Sets: With Applications to Psychology, Computer Vision and Target Tracking".

Edmund T Rolls, Department of Computer Science, University of Warwick

How the brain computes and decides

Thursday, February 24th 2011. 4pm, CS1.04

Abstract

The recognition of objects and faces in natural scenes invariantly with respect to position, size, rotation, and view is a major computational problem not solved in computer vision. How the brain computes will be illustrated by describing a hierarchical neuronal network model that is based on investigations of the functional architecture of the visual system in the brain and that performs these functions. Short-term memory attractor neuronal networks are important for attention in this system, for memory that occurs after object identification, and for decision-making. The operation of these processes enables contrasts to be made between the operation of digital computers and the computations performed by the brain. Understanding the computations performed by the brain is fundamental to understanding the operation of the brain in health and disease. Publications are available at www.oxcns.org.

Biography

Professor Edmund T. Rolls, M.A., D.Phil, D.Sc., Hon. D.Sc. is a computational neuroscientist with research interests including the operation of real neuronal networks in the brain in vision, memory, attention, and decision-making; functional neuroimaging of vision, taste, olfaction, feeding, the control of appetite, memory, emotion, and decision-making; neurological disorders of emotion; psychiatric disorders including schizophrenia; and the brain processes underlying consciousness. These studies include investigations in patients, and are performed with the aim of contributing to understanding the human brain in health and disease, and of treating its disorders. He has served as Professor of Experimental Psychology at Oxford University; Fellow and Tutor at Corpus Christi College, Oxford; Vice President, Corpus Christi College, Oxford; Secretary of the European Brain and Behaviour Society; and Secretary to the Council, European Neuroscience Association; and is an Honorary Fellow in the Department of Computer Science. He has published more than 495 full length research papers, which are shown, with many .pdfs available, at http://www.oxcns.org. His books include:

• Rolls,E.T. and Deco,G. (2002) Computational Neuroscience of Vision. Oxford University Press: Oxford.
• Rolls,E.T. (2008) Memory, Attention, and Decision-Making: A Unifying Computational Neuroscience Approach. Oxford University Press: Oxford.
• Rolls,E.T. and Deco, G. (2010) The Noisy Brain: Stochastic Dynamics as a Principle of Brain Processing. Oxford University Press: Oxford.

David Saad, Engineering and Applied Science, Aston University

The statistical physics of noisy computation

Thursday, February 3rd 2011. 4pm, CS1.04

Abstract

Contributors: Alexander Mozeika, David Saad and Jack Raymond

We show how models of random formulae can be mapped onto a physical framework and employ methods of statistical physics, developed specifically to analyse the typical behaviour of random disordered systems, to gain insight into the behaviour of noisy Boolean random formulae. The stability of the circuit towards input-layer perturbations and its dependence on the input magnetization have been studied to establish the main characteristics of the generated formulae. To investigate the properties of noisy circuits we consider two copies of the same topology with different temperatures representing the noisy and noiseless versions of the same circuit. We show that the typical-case macroscopic behaviour observed corresponds straightforwardly to the bounds obtained in the information theory literature for specific cases. Being very general, the framework is extended to consider further properties of random Boolean formulae for different gates, the level of error and function-bias expected at any depth, the sensitivity to input perturbations and expected convergence rate depending on the input bias, gate properties and gate-noise level. This framework enables one to discover typical properties of noisy computation that are inaccessible via traditional methods of information theory and complements the analysis carried out in the theoretical computer science and information theory communities.

A. Mozeika, D. Saad and J. Raymond, "Computing with Noise - Phase Transitions in Boolean Formulas'', Phys. Rev. Lett. 103, 248701 (2009).
A. Mozeika, D. Saad and J. Raymond, "Noisy Random Boolean Formulae - a Statistical Physics Perspective'', Phys. Rev. E, 82, 041112 (2010).

Biography

Professor David Saad holds degrees in both Physics (BA, MSc) & Electronic Engineering (BSc, PhD) from the Technion and Tel Aviv University. He joined the Physics Department at Edinburgh University in 1992 first as a Research Associate and later as a Lecturer. He moved to Aston University in 1995 and was appointed to a Chair in Information Mathematics in 1999. He has over 150 publications, mainly in the application of statistical physics methods and Bayesian statistics to a range of fields; these include neural networks, error-correcting codes, multi-node communication, hard computational problems, network optimisation, advanced inference methods, noisy computation and random Boolean networks. He has held over 15 research grants and is currently heading the Mathematics group at Aston.

Wolfgang Nejdl, Leibniz University Hannover

Web of People -- Improving Search on the Web

Thursday, January 27th 2011. 4pm, CS1.04

Abstract

More and more information is available on the Web, and the current search engines do a great job to make it accessible. Yet, optimizing for a large number of users, they usually provide good answers only to "most of us", and have yet to provide satisfying mechanisms to search for audiovisual content.

In this talk I will present ongoing work at L3S addressing these challenges. I will start by giving a brief overview of Web Science areas covered at L3S, and the main challenges we adress in these areas, with the Web of People as one important focal point of our research, as well as Web Information Management and Web Search.

In the second part of the talk, I will discuss search for audiovisual content, and how to make this content more accessible. As many of our algorithms focus on exploiting user generated information, I will discuss what kinds of tags are used for different resources and how they can help for search. Collaborative tagging has become an increasingly popular means for sharing and organizing Web resources, leading to a huge amount of user generated metadata. These tags represent different aspects of the resources they describe and it is not obvious whether and how these tags or subsets of them can be used for search. I will present an in-depth study of tagging behavior for different kinds of resources - Web pages, music, and images. I will also discuss how to enrich existing tags through machine learning methods, to provide indexing more appropriate to user search behavior.

Biography

Prof. Dr. Wolfgang Nejdl (born 1960) has been full professor of computer science at the University of Hannover since 1995. He received his M.Sc. (1984) and Ph.D. degree (1988) at the Technical University of Vienna, was assistant professor in Vienna from 1988 to 1992, and associate professor at the RWTH Aachen from 1992 to 1995. He worked as visiting researcher / professor at Xerox PARC, Stanford University, University of Illinois at Urbana-Champaign, EPFL Lausanne, and at PUC Rio.

Prof. Nejdl heads the L3S Research Center as well as the Distributed Systems Institute / Knowledge Based Systems , and does research in the areas of search and information retrieval, information systems, semantic web technologies, peer-to-peer infrastructures, databases, technology-enhanced learning and artificial intelligence. Some recent projects in the L3S context include the PHAROS Integrated Project on audio-visual search, the OKKAM IP focusing on entities on the Web, the Digital Library EU project LiWA, coordinated by L3S, which investigates Web archive management and advanced search in such an archive, and the FET IP project LivingKnowledge, which is developing algorithms and methods to handle and exploit diversity, bias and opinion on the Web. Another new project, GLOCAL, focuses on event-based indexing of multimedia data on the web.

Wolfgang Nejdl published more than 250 scientific articles, as listed at DBLP, and has been program chair, program committee and editorial board member of numerous international conferences and journals, most recently including the role of PC chair for WWW'09 in Madrid, PC chair for WSDM'11 in HongKong, and general chair for ICDE'11 in Hannover, see also http://www.kbs.uni-hannover.de/~nejdl/

Simon Miles, King's College London

Automatically Determining the Provenance of Data

Thursday, January 13th 2011. 4pm, CS1.04

Abstract

The provenance of something, i.e. its history or how it came to be as it is, is important knowledge in many disciplines. In science, for example, the value of a result is in part due to the rigour of the experiment which produced it, while in art collection, the authenticity of an object is judged via records of past ownership. The provenance of computed data (how the data was produced) is also important to know, particularly as computation becomes a more significant part of scientific analyses, medical diagnoses, business decisions etc. The increasing use of large scale distributed systems to process information across organisations, such as in grid computing systems, makes the problem of determining provenance both more difficult and more pressing: it is harder and more important to understand how data was processed while out of your authority. The same is true for information on the web, as data is increasingly copied or cited from one site to another. In this talk, I will give an overview of the problems of determining provenance of data in distributed systems, and the technologies which exist and are being developed to solve them.

Biography

Simon Miles is a lecturer in Computer Science at King's College London. He has worked on a range of projects in the areas of e-science, agent-oriented software engineering, electronic contracting, and distributed systems at King's and, previously, at the University of Southampton. He has experience of applying novel open systems technologies to a wide variety of real world use cases, and, as part of his work researching mechanisms for determining the provenance of data, he has collaborated with many international partners. He co-led the first two International Provenance Challenges, bringing together researchers from around twenty disparate teams in two six-month exercises to compare their systems using a single, medical application, and is on the W3C's incubator group for provenance on the web. He has published widely in the areas of multi-agent systems and e-science.

26 November 2010

Cumulative Subgoal Fulfillment: A New Approach to Developing Software

Eric Braude, Boston University

Abstract

This talk will show how a few principles of physical construction, so self-evident that they are usually unremarked, can be very useful for software construction. This talk will show how the result, formulated as Cumulative Subgoal Fulfillment, applies to classic computer science examples, to Naur's well-known but error-prone text formatting problem, to a video game, to mashups, and to linear programming.

Biography

Dr. Braude (Associate Professor of Computer Science; MS, University of Natal; MS, University of Illinois; MS, University of Miami; PhD, Columbia University) teaches software design, artificial intelligence, data structures, information system security, software engineering, and web services. His books have been translated into several languages. Dr. Braude has taught at the University of Pennsylvania, City University of New York, Pennsylvania State University and Seton Hall University, and has served as technology advisor to corporations such as Philips, Lockheed, Lucent Technologies, and MITRE Corporation.

18 November 2010

Specification

Raymond Turner, University of Essex

Abstract

The specification and implementation of computational artifacts occurs within all areas of computer science. Indeed, some would see it as the defining activity of the discipline. Consequently, unpacking its nature, and in particular the nature of specification, should form one of the central themes in the philosophy of computer science. In this talk we address some of the fundamental conceptual questions surrounding the computer science notion of specification.

It is often said that the role of specification is to describe the artifact not how to build it. While this characterization has the merit of being succinct, it hides and suggests a good number of clarifying questions.

1. What is the nature of specification? In particular, do specifications act like definitions? Indeed, do they function in the same way as definitions in mathematics?

2. Are specifications fundamentally different to computer programs? Are programs imperative and specifications descriptive? If so, how do logic, functional and object oriented programs fit into this characterization?

3. What is the relationship between a specification and an artifact? What does it mean to say that an artifact has been correctly constructed? How is correctness expressed and established?

4. What are computational artifacts? What kind of things are they?

5. How do specifications differ from scientific theories?

6. What is the difference between the specification of an artifact and the functional description of it found in a manual for its use?

While some of these issues are implicitly addressed in the relevant computational literature e.g. (Morgan, 1990; Jon 86 : Jones; Van Vliet, 2008), there is little conceptual analysis. Our aim is to contribute to the latter.

4 November 2010

Information theory of communication over multiple correlated noisy channels

Oleg Zaboronski, University of Warwick

Abstract

Motivated by the example of probe storage we consider the problem of parallel information transmission over multiple communication lines affected by strongly correlated noise. Surprisingly, channel capacity and Gallager's random coding exponent for this channel can be computed analytically. The answers show that a 'traditional' application of error correction coding to this channel will lead to an error floor for ANY code and decoding algorithm.

21 October 2010

Meet the new data model, same as the old data model

Leonid Libkin, University of Edinburgh

Abstract

In the (very) old days, the world of databases was a big mess, dominated by the network (graph) and the hierarchical (tree) data models. Then Codd came, and the nice and clean relational model replaced all others. In addition to providing a steady employment to many logicians, it created a $20billion/year business. We didn't live in that paradise for too long though: less than 30 years later, the world came back to the hierarchical model (XML). And graph-structured data hasn't been dormant all those years, although it was much less visible than the relational and XML models. Alberto Mendelzon was the first to revisit the graph model back in the 80s, and we have seen more activity lately, due to applications in areas such as RDF, biological databases, and social networks.

In this talk I shall give a few examples showing the importance of graph querying, demonstrate desirable features of graph query languages, and show which problems are easy for graph querying, and which problems suddenly become very hard.

7 October 2010

Modelling non-rigid 3D shapes

Andrew Fitzgibbon, Microsoft Research

Abstract

I will talk about modelling of 3D objects that can change shape, either in video or from sets of photos. I describe two approaches we have used recently: implicit and explicit 3D, and show how they are related. The implicit approach models the image-formation process as a 2D-to-2D transformation directly from an object's texture map to the image, modulated by an object-space occlusion mask, we can recover a representation which we term the "unwrap mosaic". This representation allows a considerable amount of 3D manipulation without ever being explicitly 3D. The second strand is to explicitly recover 3D, for example from a set of photos. Such a set might be obtained by an image search for the term "clownfish". This yields many photos of clownfish, but no two are of exactly the same individual, nor are they the same 3D shape. Yet, to the human observer, this set of images contains enough information to infer the underlying 3D deformable object class. We aim to recover models of such deformable object classes directly from images. For classes where feature-point correspondences can be found, this is a straightforward extension of nonrigid factorization, yielding a set of 3D basis shapes to explain the 2D data. However, when each image is of a different object instance, surface texture is generally unique to each individual, and does not give rise to usable image point correspondences. We overcome this sparsity using curve correspondences (crease-edge silhouettes or class-specific internal texture edges).

Biography

Andrew Fitzgibbon is a principal researcher at Microsoft Research, Cambridge, UK. His research interests are in the intersection of computer vision and computer graphics, with excursions into neuroscience. Recent papers have been on models of nonrigid motion, general-purpose camera calibration, human 3D perception, large-scale image search, and the application of natural image statistics to problems of figure/ground separation and new-view synthesis.

He has co-authored "best papers'' at ICCV (twice), CVPR, and BMVC, and software he wrote won an Engineering Emmy Award in 2002 for significant contributions to the creation of complex visual effects. He studied at University College Cork, at Heirot-Watt university, and received his PhD from Edinburgh University in 1997. Until June 2005 he held a Royal Society University Research Fellowship at Oxford University's Department of Engineering Science.

1 July 2010

The Affordances of Web 2.0/3.0 for Personal Learning Environments

Professor Hugh C. Davis, University of Southampton

Abstract

Traditionally learning has been seen as a solitary and individualistic task; learning has been represented as committing knowledge to memory and the personal acquisition of skills and literacies. The affordances of early computer technologies amplified this perspective, and transitions of learning technologies to networked platforms sustained the individualist context within the Virtual Learning Environment (VLE). However constructivist critiques of learning environments have emphasised the importance of social interactions and the benefits of groups working and problem solving as a means to learning and knowledge acquisition. Advances in Web technologies over the last decade (the so called Web 2.0) have enabled us to build tools to support and integrate many kinds of collaboration and learning in networks. Such tools have been retrofitted to existing VLEs. This presentation argues that the current generation of Virtual Leaning Environments are no longer fit for purpose; they embody an approach to learning that supports ineffective/inappropriate didactic approaches, and do not complement the expectations or approaches to learning taken by Generation Y learners.

At the University of Southampton, as part of a major curriculum innovation project we have been examining the approaches we wish to take to providing the virtual environments for learning, teaching and research that will be fit for the next ten years. The focus of this presentation will be on our reflections on personal (personalised and personalisable) rich learning environments, and the part played in these environments by Web 2.0, linked data and cloud computing.

Biography

Hugh Davis is Professor of Learning Technology within the School of Electronics and Computer Science, where he leads the Learning Societies Lab (http://www.lsl.ecs.soton.ac.uk), a research team of 50-60 people with a focus on Web Technologies and Technology Enhanced Learning. Hugh has a long history of research in the Hypertext domain going back to before the advent of the Web, and has over 200 publications (http://www.ecs.soton.ac.uk/people/hcd/publications) in Hypertext and Learning Technology, as well as numerous grants in these areas. In addition to his research, Hugh is the University Director of Education responsible for technology enhanced learning (TEL) strategy, and this combination of activities enables him to take a research informed and leading edge perspective on the technology that can be delivered at a cross university level.

24 May 2010

Personalisation in the World Wide Web

Professor Vincent Wade, Trinity College Dublin

Abstract

Personalisation web research have been successful in researching personalisation in niche application areas where web content has been specifically designed for e.g. in Tourist Information Systems, eLearning and Museum systems. More recent years has seen ‘personalisation-lite’ techniques being used by web search providers e.g. personalisation based on country of origin, or on comparison with similar or aggregate queries. However, personal use of the web extends far beyond just personalised content, and encompasses many dimensions of a web experience e.g. personalisation of tasks & activities, personalisation based on cultural preferences and values, and personalisation for social interaction and community engagement etc.

Next generation personalisation is tackling the issues of dynamic adaptation and composition of web content and services drawn from the heterogeneous open web. Such personalisation empowers the user via adaptive experiences combining traditional multimedia web content, end user generated content (wikis, ,blogs, forums, tweets, RSS feeds etc) as well as dynamically customising delivery to devices and multimodal interfaces etc.

In this seminar we will consider new directions and dimensions in personalised, adaptive web and how they can be addressed. We will investigate key challenges involving integrated open corpus & service personalisation, cultural adaptivity (including multilingual personalisation), and indicate how personalisation can enhance the web communities and the wisdom of the crowd. We will explore techniques and technology to enable multi-dimensional web personalisation i.e. personalisation of the web based on multiple, concurrent influences (from individual identity & personal properties, to context, device and service affordances).

Biography

Prof Vincent Wade: Vincent is an Associate Professor in the School of Computer Science and Statistics, Trinity College Dublin . He is Director of the Intelligent Systems Discipline which is a cluster of research groups including the Knowledge and Data Engineering Group, the Graphic Vision and Visualisation Group, the Computational Linguistics Group and the Artificial Intelligence Group as well as the Centre for Health Informatics. Vincent is also Deputy Director of the newly formed Centre for Next Generational Localisation and Personalisation (CNGL) sponsored by Science Foundation Ireland. This multi university research centre is focused on the research and development of innovative digital content management, personalization and localization on the web.

http://kdeg.cs.tcd.ie/

http://www.cngl.ie/index.html