Supervisor: Prof. Dr Helmut Veith
Microsoft Research supervisor: Byron Cook

Research title: Automatic derivation of loop bounds for worst case execution time analysis

Research summary: In many industries including robotics, consumer electronics, avionics, automotive, and manufacturing, the system components must interact according to a stringent real-time schedule. It is therefore crucial for system engineers to have a good understanding of the software execution time. Although there has been significant success in analyzing the program flow and the effects of advanced hardware features such as pipelining and cache behaviour, state-of-the-art tools work automatically only for simply structured programs. In particular, existing tools for estimating worst case execution time (WCET) have difficulties to analyze loop bounds for all but very simply structured loops. The goal of the proposed dissertation is to leverage the methods developed for Microsoft’s TERMINATOR tool for WCET analysis, i.e., for automatic derivation of loop bounds. The main challenge in the proposed work stems from the fact that state-of-the-art termination analysis methods employ quite sophisticated non-constructive mathematical methods, and do in most cases not allow to derive a loop bound directly. As argued above, a practically useful tool for the derivation of loop bounds will be valuable for embedded systems, but also for response time evaluation in a large number of software products ranging from desktop software all the way to device drivers.

Grégory Théoduloz
École Polytechnique de Lausanne, Switzerland

Microsoft Research supervisor: Byron Cook

Research title: Combining software verification and testing

Research summary: The topic of the proposed research falls within the area of software quality tools. In particular, we propose to draw on techniques from program analysis, software model checking, and automatic test-case generation, in order to develop a program verification theory and tool that combines the efficiency of testing-based approaches for finding bugs with the rigor of abstraction-based approaches for finding proofs of correctness.

Jennifer Pearson
University of Swansea, United Kingdom

Supervisor: Prof. Dr Harold Thimbleby
Microsoft Research supervisor: Richard Harper

Research title: Digital story systems

Research summary: ‘Digital stories’ were invented in Berkeley in 1994 and represent a manageable way to create compulsive audio/visual narratives. Little research has been done on them. What is the best format? What tools should be used to construct them? How can databases of stories be managed? However, it is clear that they could be used effectively for many purposes, from UCD to accident debriefing. They could be constructed on mobile phones (so there is an enormous market) except there are no tools to do so, and no user-centred development of the tools. There are three strands to this research: develop tools (to author and to manage) digital stories; to do usability studies to evaluate and improve them; to do generic studies to refine the formats of digital stories.

Jorge Peña
King’s College London, United Kingdom

Supervisor: Dr Mark Mulligan
Microsoft Research supervisors: Drew Purves, Kentaro Toyama

Research title: Novel computing methods for detailed pan-tropical water resource futures simulation

Research summary: Tropical water resources are under an unprecedented level of demand for agricultural, industrial, domestic, hydropower and navigation functions whilst also being heavily affected by continuing land use change in the tropical mountains and lowlands as well as global climate change. Tropical forests and páramos provide much of the high quality water for drinking water and hydroelectric power purposes supplying large cities throughout the tropics. Yet these areas are undergoing, significant land use change with associated detriment to both water quantity and quality. The FIESTA water resources simulation model, developed by Dr Mulligan at King’s College London, which is the most comprehensive spatial simulation model for tropical hydrology, has been used throughout Latin America to quantify water resources provided by mountain regions to populated areas in the countries as well as impacts from land use and climate change towards the assessment of the utility of implementing financial mechanisms called payments for environmental services schemes (PES) to support long lasting conservation initiatives in this areas. The project PhD will combine computing science and environmental science to further enhance the models and systems for a pan-tropical application of understanding and protecting water resources. Building on the work of my previous PhD student (joint with KCL computer science, Waleed Alsabhan, PhD completed) in developing a real time online GIS-based catchment hydrological model and incorporating our recent databases including a global database of dam locations, we will tackle these problems within the PhD in order to build, apply and make available detailed, tropics hydrological (100 m resolution) assessment data. To achieve this, significant computational and algorithms will be developed and the modelling system will be converted for use in 64-bit and parallelization computing environment. The resulting information will be made available intuitively to decision makers by using recent MS developments in online mapping (virtual earth and virtual earth 3D).

Khilan Gudka
Imperial College London, United Kingdom

Supervisor: Prof. Susan Eisenbach
Microsoft Research supervisor: Tim Harris

Research title: Optimisations for the performance of programs using atomic blocks

Research summary: The main aim of this research is to look at ways of improving the performance of atomic blocks to make them applicable for real-world software. This will be in the form of static as well as dynamic optimisations that lead to increased concurrency and better throughput with more emphasis given to multi-core/multi-CPU systems, the growing widespread availability of which is the reason for why concurrency is now of extreme importance. Most work carried out on lock inferencing has ignored the scenario of where there are multiple processing units. Furthermore, it seems evident from existing work that neither transactional memory nor lock inferencing is ‘the’ solution, given that they each have their strong and weak points and are thus more applicable for certain applications than others. Hence, an additional area to look at for increasing the performance of atomic blocks is the combination of the two approaches. This would also be looked at as part of the research. Given the current state-of-the-art, developers that require performance from their software will most probably avoid using atomic blocks. The next step is to look at improving in this area.

Nick Taylor
University of Lancaster, United Kingdom

Supervisor: Dr Keith Cheverst
Microsoft Research supervisor: Shahram Izadi

Research title: Supporting village community through connected situated displays

Research summary: The central aim of the proposed research is to understand the way in which the physical placement and design of networked displays in a rural village can influence and facilitate notions of community within the setting. It is apparent from our own research and related literature that it is essential to understand the social and physical richness of a given setting. Consequently, the planned research will draw from a range of approaches including ethnographic studies, use of cultural and technology probes, focus groups and design workshops. The proposed setting is the village of Wray in Lancashire – a small, remote village in the north of Lancashire with a population of less than 500. The planned research methodology is iterative: observe, design and deploy, observe... Where these stages are closely coupled and all hold key (technical and practical) challenges. The planned research should produce contributions in the areas of techniques for i) understanding requirements for supporting community through situated display based technologies, ii) design techniques including insights into PD techniques in this domain and the suitability of techniques such as the use of cultural and technology probes, and iii) greater understanding of the difficulties of deploying situated displays in a rural village (albeit one with enhanced connectivity).

Olga Morawczynski
University of Edinburgh, United Kingdom

Supervisor: Dr James Smith
Microsoft Research supervisors: Alex Taylor, Jonathan Donner, Nimmi Rangaswamy

Research title: An ethnography of m-payments in rural Kenya: The case of m-Pesa

Research summary: There has recently been some attention given to how mobile phone applications, such as m-payments can be used to engender local improvements. The general consensus is that these applications provide new opportunities for low-income individuals to engage in financial transactions and to increase their personal income. In this project the PhD student will engage in an ethnographic analysis of m-Pesa—an m-payment application that has recently been launched in Kenya. The student will focus on how micro-entrepreneurs in this context appropriate this application, and how such appropriation can engender local level improvements. The outcomes of this research are as follows: the dissemination of the research findings amongst Microsoft researchers in the form of reports and seminars, and the publication of research in peer-reviewed journals.

Olivier Teboul
École Centrale de Paris, France

Supervisor: Prof. Nikos Paragios
Microsoft Research supervisor: Zhengyou Zhang

Research title: Large scale 3D modelling: Confluence of computer vision and graphics and architecture

Research summary: Three-dimensional content is a novel modality used in numerous domains like navigation, post production & cinematography, architectural modelling and urban planning. These domains have benefited from the enormous progress has been made on 3D reconstruction from images. Such a problem consists of building geometric models of the observed environment. State of the art methods can deliver excellent results in a small scale but suffer from being local and cannot be considered in a large scale reconstruction process since the assumption of recovering images from multiple views for an important number of buildings is rather unrealistic. On the other hand several efforts have been made in the graphics community towards content creation with city engines. Such models are purely graphics-based and given a set of rules (grammars) as well as dictionary of architectures (buildings) can produce virtual cities. Such engines could become far more realistic through the use of actual city models as well as knowledge of building architectures. Developing 3D models/rules/grammars that are ‘image’-based and coupling these models with actual observations is the greatest challenge of urban modelling. Solving the large-scale geometric modelling problem from minimal content could create novel means of world representation as well as novel markets and applications. At the same time, like gesture analysis and facial modelling it is a great research challenge that requires an interdisciplinary effort. The main aim of our approach is to deduct very accurate models from images that are constrained from the nature of the application and then use models to solve challenging, ill-posed problems in imaging, vision and graphics.

Paul Dunphy
University of Newcastle, United Kingdom

Supervisor: Dr Jeff Yan
Microsoft Research supervisor: Michael Roe

Research title: Design and analysis of usable security mechanisms

Research summary: Despite the potential benefits of graphical passwords their design space and usability remains largely unexplored. Indeed, both theoretical and empirical studies have revealed unexpected weaknesses in some schemes. We propose to investigate a number of interleaved usability and security issues that are crucial to the real world uptake of graphical passwords. These issues include: 1) methods that can enhance both memorability and security of graphical passwords; 2) applications of proactive checking in graphical passwords, and; 3) mechanisms to counter shoulder surfing. To a lesser extent we hope to develop more ecologically valid methods to evaluate the usability of authentication mechanisms. Typically when studying the usability of passwords there is no cost to the user if they under-perform. In the real world this cost manifests itself as denial of access to some desired service e.g. internet banking. Added to his is the fact that participants are not protecting a resource of any value and so have no genuine motivation, only the reward offered by the experiment organisers. With that in mind it is hoped to develop ways to motivate participants more realistically. We hope to generate new ideas to apply to new schemes. Ultimately this will involve creation of one or more demonstrably usable and secure graphical password schemes. Our hypothesis is that graphical techniques can be just as secure, if not better than ubiquitous text passwords, in usability, memorability and security.

Philipp Hennig
University of Cambridge, United Kingdom

Supervisor: Prof. David J.C. Mackay
Microsoft Research supervisor: Thore Graepel

Research title: Probabilistic modelling for computer Go

Research summary: We propose to use probabilistic modelling to tackle the grand AI challenge of computer Go. Following recent breakthroughs in stochastic game tree search known as Monte Carlo Go, we suggest modelling the evaluations in a game tree in terms of graphical probabilistic models and view the game tree search as an inference problem. We anticipate this view to enable a better understanding of the structure of the game tree and to aid design of a strong computer go program.

Sebastian Faust
Katholieke Universiteit Leuven, Belgium

Supervisor: Prof. Dr Bart Preneel
Microsoft Research supervisor: Cédric Fournet

Research title: Provable security at implementation-level

Research summary: Traditional provable security regards cryptographic algorithms as black boxes. An adversary may have access to inputs and outputs, but the computation within the box stays secret. Unfortunately, this model often does not match reality where an adversary can attack the algorithm’s implementation with more powerful attacks. An important example in this context, are side-channel attacks, which provide an adversary with a partial view on the inner working of hardware. The goal of this project is to develop theoretical models in which formally provable security guarantees can be made concerning the implementation of cryptographic algorithms and protocols.

Simon Youssef
Ludwig-Maximilians University, Munich

Supervisor: Prof . Dr Joachim Rädler
Microsoft Research supervisors: Andrew Phillips, Luca Cardelli

Research title: Stochastic time series modelling of single cell assay data

Research summary: Single cell assays have been established recently, as a means to obtain high quality time-series data. At the same time process calculi have been inferred with stochastic simulation techniques and adapted to the needs of the systems biology community. This thesis aims at integrating both, in silico and in vitro data by providing a standard measure for comparison. This toolkit will illuminate key points of the interplay between model and experiment using all available readouts from an experimental system. Furthermore computational and experimental methods will be developed that improve the high-throughput gathering and processing of single cell data. Our method will be exemplified by applying it to the apoptosis pathway and the gene delivery process.

Tahir Mansoori
University of Oxford, United Kingdom

Supervisor: Prof. David Gavaghan

Research title: Development of a biological imaging workbench to support systems level simulation in physiology

Research summary: Our goal is to develop a suite of biological imaging tools to create an imaging workbench for the laboratory and computational scientist. Large scale, anatomically detailed simulation of biological and physiological systems is playing an increasingly vital role in our attempt to understand both normal and patho-physiology, via an iterative interplay between laboratory experiment and predictive in silico simulation. Underpinning all such simulations is the requirement for techniques to extract the necessary geometry, and to parameterise the underpinning mathematical models, ideally from non-invasive imaging techniques. The workbench, although being developed in this first instance the very mature research area of heart modelling, will find increasing application right across the life sciences. Many of the necessary tools will developed by extending existing tools in medical imaging, and this project is therefore likely to benefit from the existing collaboration between the Microsoft Research Laboratory in Cambridge and the Medical Vision Laboratory and Oxford e-Research Centre in Oxford in this area.

Usman Ali
Supélec-CNRS-University of Paris, France

Supervisor: Dr Pierre Duhamel
Microsoft Research supervisor: Bozidar Radunovic

Research title: WIBOX – A robust video receiver allowing WIMAX video broadcasting and indoor WIFI retransmission

Research summary: The proposal intends to solve most problems encountered for receiving video through a WIMAX link (even with a very weak signal) and retransmitting it indoor. The intent is to be able to build the equivalent of a ‘triple play box’ for wireless home delivery of internet services (including video streaming) through WIMAX.

Varun Gulshan
University of Oxford, United Kingdom

Supervisor: Prof. Andrew Zisserman

Research title: Inferring organization of image data using visual words

Research summary: We propose to investigate new principles for the unsupervised organization of collections of images, with application to photograph collections, image databases, and image information on the web. Existing systems for clustering or associating images tend to use global measures (e.g., histograms) which are sensitive only to gross, average properties of images, and are unable to focus on highly salient structure of a more localized nature. We plan to address this limitation by investigating the combination of two recent developments in analysis of images. The first is visual words - sparse visual features selected statistically for saliency, which have already proved powerful in video- and image-based retrieval systems. The second is hidden variable modelling that can be used to separate areas of images on the fly, so that areas of particular interest – e.g., foreground – can be selected for special treatment. These principles will be demonstrated in an experimental system for ‘power annotation’ for interactive users.

back to top