Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
2011 PhD Scholars


Aleš BizjakAleš Bizjak
IT University of Copenhagen, Denmark

Research title: Relational Reasoning for Programs Using Higher-Order Store

Supervisor: Lars Birkedal
Microsoft Research supervisors: Nick Benton, Andrew Kennedy

Research summary: The aim of this project is to research and develop relational reasoning techniques for program analyses specified via refined type systems. The reasoning techniques will be used to prove the correctness of program transformations based on the static analyses. The project will focus on programs written in programming languages with features found in modern advanced programming languages, in particular higher-order store and generics.

Alexey BakhirkinAlexey Bakhirkin 
University of Leicester

Research title: Bottom-up shape analysis with 3-valued logic

Supervisor: Nir Piterman
Microsoft Research supervisors: Josh Berdine

Research summary: Shape analysis studies how programs that make use of dynamic memory can be analysed and how their correctness can be proved. As a starting point, we take the approach of Sagiv et al., which is based on abstract interpretation and use of 3-valued Kleene logic. They described and implemented an intraprocedural analysis answering the following question: "Given a small program fragment and its possible inputs (possible values of the variables and contents of the heap at the initial program point), what heaps can arise at other program points?"

We aim to extend the approach with the ability to perform bottom-up analysis answering another question: "Given a small program fragment, what inputs make it execute without failure (terminate successfully or run forever)?" In solving this problem, we can reuse some parts of the previous work, but we also need to develop a number of algorithms that were not previously described.

Anja ThiemeAnja Thieme
Newcastle University, United Kingdom

Research title: Support of Mental Well-Being Through Technology

Supervisor: Patrick Olivier
Microsoft Research supervisor: Siân Lindley

Research summary: Cognitive behavioural therapy (CBT) is widely used by therapists to treat depression and anxiety and has been the subject of considerable empirical study, validation and clinical application. The goal of this PhD project is to design and evaluated Interactive Therapeutic Artifacts (ITAs) to support such therapeutic processes for depression. In following an experience-centered approach and combining findings of the fields of psychology, design and digital technology, it is hoped to increase individuals’ engagement in a therapeutic treatment, and thereby its efficacy and success. To empower users to interact with the treatment and to further enrich individuals’ social and emotional lives, form and function of the ITAs will be carefully considered to create and frame a very personal context for individual’s self-management, self-reflection, interaction with important others and their interpretation and appropriation of the artifacts within their daily routines.

Artem KhyzhaArtem Khyzha 
IMDEA Software Institute

Research title: Modular verification for mainstream operating systems

Supervisor: Alexey Gotsman
Microsoft Research supervisor: Josh Berdine

Research summary: An operating system (OS) kernel is the most critical piece of software running on a computer. Mainstream OS kernels implement complicated abstractions and make extensive use of multicore parallelism; as a consequence, their code is hard to get right. Formal verification can improve their reliability, and first attempts to verify small OS kernels have been encouraging. However, OS verification still remains an extremely laborious process. To make it more effective, we need verification methods tailored to this application domain that are more modular and automatic than existing ones. The aim of the proposed research is to develop novel logics and automatic tools that can reason modularly about OS kernel components, concentrating on problematic features of mainstream kernels. If successful, the proposed research will build the foundations for developing reliable operating systems. In time, its results may feed into industrial tools for OS development and verification.

Carlo SpaccasassiCarlo Spaccasassi
Trinity College Dublin, Ireland

Research title: Language Support for Communicating Transactions

Supervisor: Matthew Hennessy
Microsoft Research supervisors: Andy Gordon, Nick Benton

Research summary: Communicating transactions, a novel programming language construct obtained by dropping the isolation requirement from traditional transactions, can be used to model the combination of automatic rollback recovery and coordinated check pointing in distributed systems. We have developed a behavioural theory for communicating transactions in an abstract setting; the aim of the project is to develop the construct in a practical setting. Specifically, the project will extend concurrent Haskell with this construct, investigate how it can be efficiently implemented, identify useful programming idioms, study how communicating transactions can be combined effectively with software transactional memory, and develop verification techniques

Chandrika CycilChandrika Cycil
Dorothy Hodgkin Postgraduate Award, Brunel University, United Kingdom

Research title: AutoMedia: Family Life, Interaction and Media Use in the Car

Supervisor: Mark Perry
Microsoft Research supervisors: Abigail Sellen, Alex Taylor

Research summary: The project asks how family and home life is constituted in the car, with a particular emphasis on exploring the role and use of media. The car is a fertile environment for developing digital technologies to support driving but presents a novel site for designing human-computer interactions. Road journeys can be both stressful and enjoyable experiences, while developments in in-car media offer the potential to alleviate some of these stresses and enhance the enjoyment of travel. The role of the car in transportation and its social and physical configuration makes this setting particularly challenging as a design space. To design appropriate media, we need to understand how families inhabit their cars and the routines of social interaction that occur within them. The research investigates the car as a setting for media use in family life to develop insights for the future design of family-oriented, car-based media that are empirically grounded in examples of use.

Daniel Trejo-BanosDaniel Trejo-Banos
University of Edinburgh, United Kingdom

Research title: Machine Learning in Systems Biology: Inference and Structure Learning of Plants’ Circadian Clocks

Supervisor: Guido Sanguinetti
Microsoft Research supervisor: Christopher Bishop

Research summary: Computational systems biology is one of the fastest growing areas of research in computer science. Two of the most exciting areas have been the use and development of learning algorithms to extract information from data, and the application of formal methods to rationalise the behaviour of biological systems. The aim of this project is to develop machine learning tools which can handle inference in the continuous-time dynamical systems underlying the theoretical computer science approach to systems biology, and apply these novel methodologies to the modelling and understanding of biological clocks in plants (in collaboration with the Millar lab at Edinburgh). Besides providing novel biological and methodological insights, it is envisaged that this project will contribute to lay the foundations for cross-fertilisation between machine learning and formal methods research in systems biology, capitalising on the exceptional strength in both fields both at Edinburgh and at Microsoft Research

Elena Tretyak Elena Tretyak
Max-Planck Institute for Computer Science, Germany

Research title: Physically Motivated Scene Understanding

Supervisor: Peter Gehler
Microsoft Research supervisor: Carsten Rother

Frits DannenbergFrits Dannenberg
University of Oxford, United Kingdom

Research title: Automatic Verification Techniques for DNA Computing

Supervisor: Marta Kwiatkowska
Microsoft Research supervisor: Andrew Phillips

Research summary: DNA computing is a new and fast-growing field that aims to engineer artificial computing devices using bio-molecular materials such as DNA. Potential applications for this technology include autonomous molecular processes that can diagnose and respond to diseases within living cells. It is an inherently interdisciplinary area that brings together, amongst others, molecular biology and computer science. This project proposes to develop formal verification techniques for DNA computing that can rigorously check the correctness of designs and identify flaws before they are implemented. Furthermore, quantitative verification techniques will be developed, that can analyse a wide range of quantitative properties, such as the likelihood of a flaw occurring in a DNA circuit design or the time required for a computation to execute. The goal is to develop scalable and efficient new verification techniques, built into software tools that will help automate DNA computing design processes.

Guy Golan GuetaGuy Golan Gueta
Tel Aviv University, Israel

Research title: Enforcing Atomicity for Data Structure Manipulations

Supervisor: Mooly Sagiv
Microsoft Research supervisor: Byron Cook

Research summary: Sophisticated data structure implementations play a key role in the performance of many software systems. Concurrency significantly increases the challenge of developing such implementations. An interesting question is how to automatically enforce atomicity and linearizabilty, while also guaranteeing other desirable properties such as: disjoint parallelism, deadlock freedom, scalability, and good practical performance. We propose to ease the task of designing concurrent data structures tailored to given applications by combining user-abstractions of the intended system behavior together with efficient compile-time and run-time techniques which enforce these abstractions on existing and future systems.

Istvan HallerIstvan Haller
Vrije Universiteit Amsterdam, The Netherlands

Research title: Security for Legacy Binaries

Supervisor: Herbert Bos
Microsoft Research supervisor: Manuel Costa

Research summary: Security in legacy binary systems is only as strong as the weakest link. The weakest link is often some obscure, older library or program that is vulnerable to memory corruption attacks. In this project, we work towards the protection of legacy binaries against memory corruption attacks, while assuming no knowledge of the binary’s source code, no symbol tables, and no help from the software vendor. Moreover, we aim specifically at stripped C binaries for x86-based architectures. We retrofit security in such binaries by first extracting the program's data structures (by means of dynamic analysis), and then rewriting the binary to guard all accesses to these structures (so that they do stray beyond the buffer boundaries). To do so, we will conduct research in data coverage (to exercise all data structures), reversing of compiler optimizations, and finally rewriting binaries to harden them against buffer overflows.

Ján MargetaJán Margeta
INRIA, France

Research title: Automatic Indexation of Time-Series 4D Cardiac MR Images

Supervisor: Nicholas Ayache
Microsoft Research supervisor: Antonio Criminisi

Research summary: This project is about searching through large databases of medical images efficiently. Specifically, given a database of 4D cardiac MR images of patients stored with an expert diagnosis, we wish to select automatically the most similar cases to the cardiac images of a new patient. Similarity must be computed as a function of image content alone so as to negate the need for expensive manual textual tagging.

Jenny VuongJenny Vuong
University of Reading, United Kingdom

Research title: Testing 3D and View-Based Models of Human Navigation

Supervisor: Andrew Glennerster
Microsoft Research supervisors: Andrew Fitzgibbon, John Winn

Research summary: Accurate modelling of human performance in navigation and other spatial tasks is of great interest in the field of human visual perception, and successful models are likely to influence future work in related fields such as machine vision and SLAM. This project will explore computational models for two competing hypotheses—view-based representation and 3D reconstruction—to determine which provides the best account of human performance on a navigation task. Experimental participants will carry out small-scale "homing" tasks in a state-of-the-art immersive virtual reality environment. Errors recorded under a range of conditions will be compared to predictions of (i) a view-based model in which observers try to match visual parameters in their initial and final views and (ii) a 3D reconstruction model in which observers try to match their location in a 3D reference frame. This will be the first detailed, direct test of view-based versus 3D reconstruction models in human vision.

Karthik Nilakant
University of Cambridge, United Kingdom

Research title: D³N: Data Driven Declarative Networking in Dynamic Mobile Networks

Supervisor: Eiko Yoneki
Microsoft Research supervisor: Christos Gkantsidis

Research summary: Demand on programming in dynamic mobile networks as versatile services is increasing. The intersection between networking and programming languages is an emerging active research topic in this context, and it is crucial for us to explore new programming paradigms in the networking space that allow the use of such future emerging networks. The proposed project aims at addressing these issues by introducing a declarative networking programming paradigm, i.e. Data Driven Declarative Networking (D³N), where communication resources are managed together with network connectivity. It includes provision of an expressive language for building applications for distributed computation. D³N will be implemented in a functional language that provides an intermediate abstraction between implementation detail and reasoning about logic flow. D³N implementation targets mainstream functional languages, including verification and compiler construction targeting to various platforms in mobile devices.

Ken WangKen Wang
University of Oxford, United Kingdom

Research title: Spatially-Resolved Representation of Sarcomeric Membrane Structures and Function for Incorporation into Computational Cell Model

Supervisor: David Gavaghan
Microsoft Research supervisors: Hillel Kugler, Neil Dalchau

Research summary: Computational modelling of the heart is perhaps the most mature area of systems biology. The representation of physiological and pathological behaviour of the heart critically depends on the way in which the behaviour of individual cardiac cells is modelled. Cardiac cell models are still inadequate to address many key scientific questions, in particular where related to translation of molecular level insight to the prediction of organ behaviour in health and disease. In this project we will build on ground-breaking research in the laboratories of Dr’s P. Kohl, A. Hoenger and R. Winslow, to provide geometrically-detailed nanoscopic data on heart cell structure and function. This will be used to build a full 3D spatially-resolved model of the cardiac sarcomere which will be implemented in the in-house developed Chaste package, one of the fastest open source solvers available for the partial differential equations modelling cardiac behaviour.

Kumar SharadKumar Sharad
Dorothy Hodgkin Postgraduate Award, University of Cambridge, United Kingdom

Title: Unifying Isolation Technologies to Protect Personal Information

Supervisor: Steven Murdoch
Microsoft Research supervisor: George Danezis

Research summary: Users of the Internet are subject to increasing levels of surveillance, harming privacy and deterring the use of the Internet for sensitive activities. There is a growing desire for tools to protect individuals, but progress in this are is hampered by fundamental gaps in knowledge. The core concept behind protecting the privacy of Internet users is "unlinkability," i.e., making it difficult to link actions to the identity of the person who carried it out. Where some action is sufficiently distinctive such as to uniquely identify who carried it out (a pseduo-identifier) they must also be unlinkable to other actions. Systems which enforce this unlinkability are known as isolation technologies, but there is no one system which can provide adequate protection by itself. Moreover, the composition of such tools may be insecure even if individual ones are secure. This project will link such tools such that their composition is secure, though capability-based access control.

Mahmoud AwadMahmoud Awad
Queen's University Belfast, United Kingdom

Research title: AGE – Adapted Games for the Elderly

Supervisor: Cathy Craig
Microsoft Research supervisors: Richard Harper, Otmar Hilliges

Research summary: A healthy mind in a healthy body is key to successful ageing. Can computer games actually help keep us healthy? This study will look at how working with the end user (i.e. older adults) can inform the design of new computer based games that will train the body (through the movements required to play the game) and the mind (having different cognitive tasks that require bodily movement to select the correct answer). By including older adults in the consultation and inclusive design process we will see how the latest motion based gaming technology can be used to create adapted computer based games. By profiling the action capabilities of the older user, the actions required to play the game can automatically be adjusted. This will ensure the best possible user experience for older adults with the added advantage of health benefits from exercising both the body and mind. It is hoped that the principles of game design developed from this project, can be transferred to other domains.

Martin Kiefel
Max Planck Institute for Intelligent Systems, Germany

Research title: Intrinisic Image Layers for Image Editing

Supervisors: Bernard Schölkopf, Peter Gehler
Microsoft Research supervisor: Carsten Rother

Michael HornacekMichael Hornacek
Vienna University of Technology, Austria

Research title: 3D Scene Completion

Supervisor: Margrit Gelautz
Microsoft Research Supervisor: Carsten Rother

Research summary: Creating novel views from a sparse set of input images has been a long-standing goal in computer vision. Applications are vast (e.g. games, Photosynth, 3D image manipulation), especially in the light of latest hardware developments (3D TV, stereo cameras). We revisit this fundamental problem from a new perspective. A major challenge for new view synthesis is to reconstruct both the depth and the colour of those pixels which have not been observed in any of the input images. We term this problem 3D scene completion. Our hypothesis is that by extracting and modelling physically aspects of the scene, such as geometry, light and camera, it is possible to improve on competing methods which operate purely in the image space. The key insight is that the methods and models used to solve the completion task are highly dependent on the physical aspect. We further believe that a joint estimation of various scene aspects is possible and superior to solving the problems independently.

Miguel LurgiMiguel Lurgi
Instituto Ciencias del Mar, Barcelona, Spain

Research title: Contrasting Assembly and Disassembly of Ecological Networks in a Changing World

Supervisor: José Montoya Teran
Microsoft Research supervisors: Drew Purves, Lucas Joppa

Research summary: The study of species interaction networks provide important insights into how ecosystems are built up (assembly) and whether and how they may collapse (disassembly) under current global change. The relationship between assembly and disassembly processes and trajectories is little understood, with many studies assuming that the effects of species loss or gain are symmetric and interchangeable. Assembly and disassembly studies have not considered the role of evolutionary processes in shaping current ecological networks and in explaining network robustness to species loss respectively. Processes of niche specialization and differentiation producing adaptive radiations have been neglected. Our aim is twofold: first, to develop individual-based evolutionary network assembly and disassembly models to predict network patterns and the effects of biodiversity loss. And second, to contrast whether, when, and how, the assembly and disassembly of ecological networks show different trajectories.

Oliver BatesOliver Bates
Lancaster University, United Kingdom

Research title: Home Activity Sensing for Energy Monitoring and Home Automation

Supervisor: Mike Hazas
Microsoft Research supervisor: James Scott

Olle FredrikssonOlle Fredriksson
University of Birmingham, United Kingdom

Research title: Structural Foundations for Heterogeneous Computation

Supervisor: Dan Ghica
Microsoft Research supervisor: Nick Benton

Research summary: We will develop technologies for the efficient mapping of high level programming languages to heterogeneous computing platforms. We are focused on support for functional aspects of languages, which present conceptual and technical challenges in this unconventional setting, using innovative semantical models. Theoretical work will be practically validated using a proof-of-concept heterogeneous compiler. The main aims of the research are theoretical (a location-aware semantics of programming languages), technological (type-enforced protocols for inter-processor communication) and applicative (an experimental hardware compiler enhanced with heterogeneous features).

Rebecca SpriggsRebecca Spriggs
University of Cambridge, United Kingdom

Research title: Inferring Forest Structure and Disturbance Dynamics by Combining a Canopy Model with LiDAR Remote Sensing Data

Supervisor: David Coomes
Microsoft Research supervisors: Matthew Smith, Drew Purves

Research summary: Large amounts of tree and forest data are needed to properly include stand- and landscape-level processes within models of the terrestrial carbon cycle. Light detection and ranging (LiDAR), a recent remote sensing technology that returns a high-resolution description of the canopy surface across forested areas, can help meet this need by scaling between plot-based measurements of individual trees, and the structure and dynamics of broad landscapes. We propose to combine a recent model of canopy structure with LiDAR data to (1) map the number, size, and distribution of trees across a temperate forest landscape with greater accuracy than previously possible; and (2) use this new method to infer the size and intensity of recent disturbances on this landscape. By mechanistically linking remote sensing data to individual trees, this project will help enable improved modelling of carbon stocks and fluxes that realistically represents the processes of tree growth, mortality, and disturbance.

Robert NortonRobert Norton
University of Cambridge, United Kingdom

Research title: Exploring Hardware Support for Multithreading and Message Passing

Supervisor: Simon Moore
Microsoft Research supervisor: (to be appointed)

Research summary: Hardware mechanisms to handle events and schedule an arbitrary number of threads will be investigated. These will replace low-level tasks traditionally performed by the operating system. We hypothesise that such hardware mechanisms will result in applications running at higher performance whilst using less power. By making threading inexpensive (unlike current commercial processors), we should open up new strategies for implementing parallel applications. The expected outcome is a system capable of emulating at least a 1,000-core system, including mechanisms to profile its behaviour. Planned collaboration with Microsoft Research will facilitate the analysis of future application requirements, operating system techniques, and approaches to profiling parallel systems.

Sandro BauerSandro Bauer
University of Cambridge, United Kingdom

Research title: Knowledge Discovery and Extraction from Large-Scale Entity-Relationship Networks

Supervisor: Stephen Clark
Microsoft Research supervisor: Thore Graepel

Research summary: Current search engines are poor at answering queries regarding named entities. Web users are naturally interested in relationships between people, people and locations, people and times, and so on. For example, a user wanting to discover information about Einstein has to type the name into a search engine, and is then given a link to the relevant Wikipedia page, from which the information has to be manually extracted. Worse still, if the user wishes to know the relationship between Einstein and Eddington, the search engine can only return single pages mentioning both names, which may or may not be informative. The aim of this project is to enable knowledge extraction and discovery from entity-relationship networks. The focus of the project will be on a) building large-scale entity relationship networks using state-of-the-art language processing tools; b) developing efficient algorithms for querying these networks; and c) developing suitable methods for evaluating the acquired knowledge.

Simo HosioSimo Hosio
University of Oulu, Finland

Research title: Social Networking Services for Public Spaces

Supervisor: Jukka Riekki
Microsoft Research supervisor: Richard Harper

Research summary: We aim to augment public physical spaces with co-located users' selected online social media content. We believe that this will increase awareness and interaction among people present in public physical spaces, and positively affect to the user experience of the space itself. This work will generate new knowledge on presenting personal content in casual public spaces, such as cafes or malls, and produce mechanisms for situated control of personal content exposure settings in these spaces, i.e., situated privacy settings for online social media content. We will explore both public screens (displays, projectors, etc.) and mobile interaction devices for displaying and interacting with the content and the people. We can realistically evaluate research prototypes, as we have already a wide infrastructure, including interactive public displays, sensor networks, and communications middleware, available in an authentic urban city setting, used by thousands of real end users.

Simon Lyons
University of Edinburgh, United Kingdom

Research title: Learning and Inference in Highly Structured Continuous-Time Stochastic Systems

Supervisor: Amos Storkey
Microsoft Research supervisor: Christopher Bishop

Research summary: Many real-world systems are well described by continuous-time stochastic differential equations. For known distributions, there exist techniques for integrating the equations forward through time and hence evaluating (a probability distribution over) future predictions. A more challenging problem, but one of huge practical importance, is to reverse this process and to infer the nature of the unknown probability distributions given a set of observed time sequences. More generally still, the structure of the equations (for example, the presence or absence of particular interactions) is also unknown, and again we would like to infer such structure from observations. Typical analysis techniques used for inference and learning in many applications of this form are either discrete time methods or use deterministic ordinary differential systems, despite significant deficits of both these approaches. The primary aim of this project is to develop new practical, generally applicable techniques for continuous-time stochastic inference for both discrete-state and continuous-state systems; these methods will then be demonstrated in particular important application areas and will be provided as C++ libraries that will be promoted for wider dissemination of the methods. The result will be to develop improved methods for inference and learning in continuous time stochastic systems, and to allow continuous time stochastic methods to be used in many real problems with greater ease.

Thi Vân-Anh NguyenThi Vân-Anh Nguyen
GREYC, France

Research title: Multi-Stage Constraint Programming

Supervisor: Arnaud Lallouet
Microsoft Research supervisor: Youssef Hamadi

Research summary: Multi-agent decision under uncertainty as encountered in sustainable development applications has raised new challenges in optimization. Not only is needed to find optimal value for a static problem but also for situations in which several agents have their own goals and interact by sharing some resources. We propose to address this latter category of problem by introducing a multi-agent multi-level optimization language based on quantified and stochastic programming. Three aspects will be addressed: modelling, solving, and applications.

Uwe SchmidtUwe Schmidt
Technische Universität Darmstadt, Germany

Research title: Learning Expressive Conditional Random Fields for Image and Scene Modeling

Supervisor: Stefan Roth
Microsoft Research supervisor: Carsten Rother

Wei PanWei Pan
Dorothy Hodgkin Postgraduate Award, Imperial College London, United Kingdom

Research title: Automatic Robust Output Maximisation of Arbitrary Synthetic Biological Circuits In-Vivo

Supervisor: Guy-Bart Stan
Microsoft Research supervisors: Andrew Phillips, Neil Dalchau

Research summary: Synthetic biology is a newly emerging field with huge potential for a paradigm shift in the way that biology is conducted and how it is used. Beyond manipulating cells to understand existing biological functions, synthetic biology endows cells with new functions (e.g., production of biofuels or medicine), by inserting biological "parts" into a host cell. However, by performing non-endogenous functions, the fitness of the host cell may diminish, limiting its capacity to perform the new functions. Rather than attempting to set an optimal activity a priori, we propose that automatic regulation of the circuit may be achieved via feedback control. This has the advantage of providing robustness to perturbations, such as variations imposed by gene expression and the host cells environment. The design will combine the GEC software and H-infinity control analysis. Automatic robust optimal control would improve synthetic circuit yields, a key requirement for profitable biotechnologies.

Xiaokun WuXiaokun Wu
Max-Planck-Institut für Informatik, Germany

Research title: Scene Understanding by Global Structure Inference

Supervisor: Thorsten Thormählen
Microsoft Research supervisors: Andrew Blake, Pushmeet Kohli

Research summary: With the emergence of modern fast acquisition devices, we can easily acquire scanning data in point format by much simplified automatic operations. However, due to cost-effect limitations, and constrained environmental conditions, the data quality is often quite low, with presence of noise and in-completion. It is a great challenge to understand the data and interpret the scene with traditional local geometric analysis, since those methods highly rely on continuous or even high order differential computations, which are unstable or completely incomputable under current input conditions. We argue that global structures inferred from parts’ correspondence are the key to solve this problem. Observing that for limited manufacturing process and aesthetic considerations, man-made objects often present high regularities in both shape composition and configuration. We propose algorithms which consider both local geometric properties, and global relations to solve a broad aspects of scene understanding problem. Applications include geometric reconstruction, content creation, and object arrangement.