Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
2008 PhD Scholars
 
Calum BrownCalum Brown
University of St Andrews, United Kingdom

Supervisor: Dr. Janine Baerbel Illian
Microsoft Research supervisor: Drew Purves

Research title: Spatiotemporal analysis of complex ecological communities

Research summary: Ecologists have presented a variety of models to explain community structure, relative abundance, and species coexistence in biodiverse communities. This project tests the hypothesis regarding whether the neutral model and niche differentiation leave different footprints in multi-species spatial patterns of competing species. Stochastic, agent-based models are developed to generate multi-species spatial patterns under contrasting assumptions of neutrality and niche differentiation and statistical measures from spatial point process theory are derived to characterize the main features of multi-species spatial patterns. These statistical measures are applied to the multi-species spatial patterns generated by the agent-based models, to see how the footprints of different model assumptions can be distinguished. It will then apply the statistical measures to spatial patterns of trees in tropical rain forests to examine the extent to which the multi-species patterns are consistent with different assumptions about neutrality and niche differentiation.

Catalin HritcuCatalin Hritcu
Saarland University, Germany

Supervisor: Prof. Michael Backes
Microsoft Research supervisor: Andy Gordon

Research title: The Secure Implementation of Cryptographic Protocols

David HopkinsDavid Hopkins
University of Oxford, United Kingdom

Supervisor: Prof. Luke Ong
Microsoft Research supervisor: Andrew Kennedy

Research title: Verifying properties of the ML family of programming languages

Research summary: We aim to develop verification techniques for higher-order (call-by-value) procedural languages with reference type, as exemplified by Ocaml, F#, and other members of the ML family of programming languages. Specifically we set ourselves the following tasks:

    • Derive an algorithm for deciding observational equivalence (of an appropriate fragment of Reduced ML) by reduction to the equivalence of visibly pushdown automata, and build a prototype implementation of it.
    • Develop a notion of reachability test for higher-order procedural languages, identify language fragments for which it is decidable, and determine its complexity.
    • Construct algorithms that symbolically compute over-approximations of an appropriate collecting semantics for higher-order procedural languages, with a view to the data and control flow analysis of these programs.

Davide CacchiarelliDavide Cacchiarelli
University of Rome 'La Sapienza', Italy

Supervisor: Prof. Irene Bozzoni
Microsoft Research supervisor: Jasmin Fisher

Research title: High complexity cell networks involving microRNAs: A systems biology approach

Research summary: microRNAs are a large class of small non-coding RNAs, which regulate gene expression at the post-transcriptional level through base-pairing with the 3’-untranslated region (3’UTR) of target messenger RNAs (mRNA). miRNAs are a considerable part of the transcriptional output of the genomes of plants and animals, involved in the establishment of complex circuitries acting in many different phases of development and differentiation. It is currently estimated that miRNAs account for ~1 percentof predicted genes in higher eukaryotic genomes and up to 30 percentof the genes might be regulated by miRNAs. We are witnessing a shift in our understanding of the complexity in gene regulatory networks caused by the discovery of miRNAs. This PhD project joins the efforts of two research groups, an RNA molecular biology group and a bioinformatics group. The goal of the collaboration consists of analyzing several aspects of miRNA genomics, expression and activity, from the computational biology predictions, to the biological validation of inferences. Existing and new data will be integrated in a computational study aimed at simulating and drawing new cellular networks mediated by non coding RNAs. A successful approach to unravel the phenotypic role of individual miRNAs consists of detailed experimental studies applied to various model systems. Importantly, the problem can also be approached by computational methods, as we propose in this project. In summary, the target of this PhD project is threefold:

      • According to the experimental findings of our molecular biology laboratory and by means of a computational approach, we intend to identify not yet known rules underlying RNA-protein interactions.
      • We propose to build specific clusterization methods to manage the great amount of data obtained from global gene expression assays performed in our experimental lab and retrieved from public databases (both miRNA and mRNA expression data).
      • The collected data will be used to identify new cellular regulatory circuitries involving miRNAs and mRNA.

Elias AthanasopoulosElias Athanasopoulos
Foundation for Research and Technology–Hellas (FORTH), Greece

Supervisor: Prof. Evangelos Markatos
Microsoft Research supervisor: Thomas Karagiannis

Research title: On the misuses of real world large scale distributed systems

Research summary: Distributed systems dominate in real world applications. Apart from the e-mail system or the World Wide Web, which are considered as large-scale distributed systems, other systems exist providing different applications to the end user. Systems for file sharing, video casting, social networking, and Voice over Internet Protocol (VoIP) are some examples of online communities that are composed by thousands of independent computer nodes. A significant number of these systems operates by using the peer-to-peer (P2P) paradigm. These systems are built over the cooperation of different computer entities and no central mechanism is used to instrument their operation. Such systems can be misused in order to provide different operations than the ones for which they were designed. More precisely, these online communities can be used as attack platforms against any computer that is connected to the Internet. In this project, we seek to develop a generic framework, that is capable of identifying these vital properties that make a distributed system vulnerable to possible misuse.

Emily LinesEmily Lines
University of Cambridge, United Kingdom

Supervisor: Dr. David Coomes
Microsoft Research supervisor: Drew Purves

Research title: Predicting long-term forest dynamics at regional scales: constraining models with data

Research summary: The response of forest ecosystems to climate change is a major source of uncertainty in predictions of future climate. The project will use novel Bayesian methods, in conjunction with very large ecological data sets, to estimate a complete set of forest simulation model parameters for each of the major tree species over a large Mediterranean region (Spain). Model simulations will then be used to test various hypotheses about the climatic control of vegetation, and to predict the potential response of Spanish forests to future climate change.

Eno TöppeEno Töppe
TU Munich, Germany

Supervisor: Prof. Daniel Cremers
Microsoft Research supervisor: Carsten Rother

Research title: Vision for graphics – High level image manipulation using uncertain preimages

Research summary: Manipulation and editing of photographs has moved from Hollywood and professional photography studios into the home. We want to turn our photographs from mere factual records into evocative mementos—even into works of art. However, despite the great leaps in usability that digital image editing allows, most existing software (whether commercial or in research papers) is focused on low-level editing (erasing, cut and paste, and so forth). The challenge addressed by this research proposal is to allow for editing on a higher level of image interpretation. Although such systems have been suggested many times, they fall at the first hurdle: We cannot build reliable algorithms to recover high-level information—such as shape, lighting, object identity, or even camera settings (aperture, focus, and so forth)—from real-world images. The reasons for this are not simply that existing algorithms must solve a complex optimization problem, but that the images themselves are ambiguous: many 3D scenes (or preimages) may give rise to the same image. For example, under different lighting, a shiny cylinder may look identical to a nearly matt prism. We propose to incorporate this uncertainty into common editing tasks explicitly, marginalizing over the probability distribution on preimages to accomplish the following:

    • Generate realistic edits despite uncertain scene interpretations.
    • Guide the user in choosing among equivalent preimages, but only to the extent necessary to complete each editing task.

Enuo HeEnuo He
Dorothy Hodgkin Postgraduate Award
University of Oxford, United Kingdom

Supervisors: Prof. Béla Novák and Dr. Andrew Dalby
Microsoft Research supervisor: Andrew Phillips

Research title: Stochastic modelling of the yeast cell cycle

Research summary: In the cell division cycle, cells replicate their DNA, segregate the duplicated sister chromatids and divide into two daughter cells. The unidirectional repetitive of cell cycle is one of the essential features to maintain proliferation of life. The irreversibility of cell cycle transitions is controlled by a complex network containing cyclin-dependent protein kinases (Cdks) and their regulators. Budding yeast due to its special genetic characters has been intensively studied both experimentally and in sillico. In particular, a large number of deterministic models have been developed for its cell cycle regulations based on ordinary differential equations (ODEs). Recently, a trend of using stochastic techniques has been spotted in this field. The main advantage of stochastic methods is that it is able to capture the noise and fluctuations that are ubiquitous in the cells.

The purpose of this work is twofold: first, we study and formulate the existing deterministic Novak-Tyson model in terms of elementary chemical reactions, which can be properly simulated using stochastic algorithms (e.g., SSA, chemical Langevin equations, etc.). In the second part, we will focus on dynamic features and the effects of noise in our model by comparing different stochastic simulation outcomes. We plan to enrich our stochastic model with explicit representations of more completed cell cycle networks and try to explain more observations in specific experimental conditions by employing different stochastic techniques.

François DupressoirFrançois Dupressoir
The Open University, United Kingdom

Supervisor: Dr. Jan Jürjens
Microsoft Research supervisor: Andy Gordon

Research title: Verifying implementations of security protocols in C

Research summary: One of the successes of formal methods in computer security is the development of tools to analyze abstract specifications of cryptographic protocols against high-level security requirements (such as confidentiality, privacy, and authenticity properties). Despite recent advances in analyzing the implementation code of security protocols [JY05,GP05,BFG06,BFG06a,Gor06,Jur06,Jur07], there are no tools shown to analyze pre-existing protocol implementations in C against high-level security requirements, although tools to check lower-level properties, such as memory safety, do exist. Inventing tools to verify high-level properties of the code—as opposed to abstract specifications—of security protocols is important: in part, because implementation code is often the first and only place where the full details of a protocol are formalized, and in part because even if there is a detailed formal specification, the implementation may introduce additional vulnerabilities. The goal is to start with pre-existing implementations of cryptographic protocols and to verify them against security properties by using formally sound yet practically usable analysis techniques and tools. An important objective is to ensure that these analysis methods are practical by keeping the overhead of their use as small as possible. First, they take input artifacts that are already available in current industrial software development (the program source code). Second, the tools should be reasonably easy to use and have a strong emphasis on automation. Manual effort (such as inserting annotations into the code) should be minimised. The goal of the security analysis is to find code vulnerabilities that give rise to attacks within the Needham-Schroeder threat model (such as man-in-the-middle, replay, or impersonation attacks). The project does not primarily aim to detect buffer-overrun vulnerabilities, as there many existing techniques (including the CCured tool) for detecting or mitigating such problems. Our main aims are to develop a formal security verification methodology to verify implementations of cryptographic protocols in C against security properties, such as confidentiality and authenticity, and to apply the methodology to the implementation of a widely-used security protocol (such as the Internet security protocol standards SSL/TLS, SSH, or Kerberos).

Iain WhitesideIain Whiteside
University of Edinburgh, United Kingdom

Supervisor: David Aspinall
Microsoft Research supervisor: Georges Gonthier

Research title: Proof engineering: refactoring proof

Jagadeesh GorlaJagadeesh Gorla
Dorothy Hodgkin Postgraduate Award 
University College London, United Kingdom

Supervisor: Dr. Jun Wang
Microsoft Research supervisor: Stephen Robertson

Research title: Unified relevance models for information retrieval

Research summary: In information retrieval, relevance is a very important concept and has been heavily studied. There are two different views on how to assign a probability of relevance of a document to a user need, namely document-oriented and query-oriented views. The classic probability model of information retrieval takes the query-oriented view, while the language modeling approach to information retrieval builds upon the document-oriented view. However, neither view represents the problem of information retrieval completely. This proposed PhD research programme aims at breaking the partial views that exist in current retrieval models, and formally develop a new retrieval paradigm that explores more of the dependency in the data and unifies evidence from different information sources to improve retrieval performance. To achieve our goal, we will do the following:

      • Explore the dependency between users who have similar information needs
      • Combine evidence from different information sources
      • Apply Bayesian probabilistic approaches to model the unified relevance

James Auger
Royal College of Art, United Kingdom

Supervisor: Prof. Anthony Dunne
Microsoft Research supervisor: Alex Taylor

Research title: Human/Robot Cohabitation: an interaction-focused approach to designing robots for the home

Research summary: Over the coming years, robots are destined to play a significant part in our daily lives. However, how will we interact with them? What kind of new interdependencies and relationships might emerge in relation to different levels of robot intelligence and capability? Given a choice, what would we like to happen and how would we like our robots to exist in our homes? This project will explore and develop new interactions between people and robots and use them as a starting point for robot design.

Jurgen Van Gael Jurgen Van Gael
University of Cambridge, United Kingdom

Supervisor: Prof. Zoubin Ghahramani
Microsoft Research supervisor: Ralf Herbrich

Research title: Machine learning models for large-scale systems and networks

Research summary: In the past 15 years, some of the most beautiful and useful machine learning tools have been motivated by problems in biology, natural language processing, computer vision, and other fields. In all these areas, statistical approaches have been crucial for dealing with uncertainty. In this application, we propose to explore new directions in statistical machine learning motivated by challenging problems in the field of computer systems and networking.

Laura Dietz
Max Planck Institute for Software Systems, Germany

Supervisor: Prof. Dr. Tobias Scheffer
Microsoft Research supervisor: Ralf Herbrich

Research title: Probabilistic Topic Models to Support a Scientific Community

Mariano Díaz
Dorothy Hodgkin Postgraduate Award
Imperial College London, United Kingdom

Supervisor: Dr. Radhika Desikan
Microsoft Research supervisor: Jasmin Fisher

Research title: Modelling integrated signalling networks in stomatal guard cells

Research summary: Stomata are microscopic pores on the surface of leaves that control water and gas exchange between the plant and the environment. It is estimated that around 65 percent of the Earth’s fresh water passes through these stomatal pores in plants. With global climate change and the lack of availability of water in several parts of the world, an increased understanding of how plants regulate stomatal closure potentially has a significant impact on plant yield and productivity. Stomatal closure occurs in response to a number of input signals, including drought stress, pathogen attack, hormone challenge, humidity, and high carbon dioxide. Guard cells surrounding stomata are highly specialised cells that control the opening and closing of the stomatal pore. A number of signalling pathways that occur in guard cells in response to each of the stimuli mediate the outcome, stomatal closure. Although much research efforts are focused on studying the effects of a single stimulus (for example, the hormone abscisic acid, made in response to drought stress) on stomatal apertures, there is little known about how different stimuli interact to regulate stomatal apertures. It is the purpose of this project to understand, via modelling, how combined signals lead to a cellular response different to that derived from a single stimulus. Ultimately, it will lead to an increased understanding of plant behaviour in response to multiple environmental stresses and the design of better experiments that help reduce water loss from plants. Using available data, it is proposed that construction of simple models to understand signal integration in guard cells will help predict subtle cellular changes in response to the environment. The project will aim to build a model: to help identify which of the key “nodes” already identified are essential for signal integration; to understand how disruption of one signalling pathway can lead to a maximum change in output; and ultimately, to be able to predict a change in the output with variations in input signals.

Masoud Koleini
University of Birmingham, United Kingdom

Supervisor: Dr. Mark Ryan
Microsoft Research supervisor: Moritz Becker

Research title: Verification of statebased access control

Research summary: We aim to provide a method that allows fine-grained decentralised access control systems to be verified against abstract high-level properties of a kind that can be set and understood by managers. This kind of verification will give assurance of the correctness of the low-level ACS. We will build a modelling language that supports decentralised systems, delegation, roles, and statebased permissions; and a method for verifying systems described in that language against abstract policies. If time permits, we will also explore whether fine-grained access control systems can be synthesised from the high-level properties.

Mehdi Hosseini Mehdi Hosseini
Dorothy Hodgkin Postgraduate Award
University College London, United Kingdom

Supervisor: Prof. Ingemar Cox
Microsoft Research supervisor: Natasa Milic-Frayling

Research title: Understanding resource-constrained information retrieval

Research summary: Search engines need to index a huge amount of data (billions of Web pages) and must deal with very high query loads (hundreds of thousands of requests per hour). This places serious strains on the underlying computer systems. This proposal seeks to develop a theoretical framework in which to understand the tradeoffs between performance and cost, where performance is measured with respect to the quality of the retrieved results and cost is a function of hardware costs and economic costs associated with degraded performance. The theoretical developments will be supported by empirical studies to verify the theoretical models and guide the development of improved models.

Mihhail AizatulinMihhail Aizatulin
The Open University, United Kingdom

Supervisor: Dr. Jan Jürjens
Microsoft Research supervisor: Andy Gordon

Research title: Verifying implementations of security protocols in C

Research summary: One of the successes of formal methods in computer security is the development of tools to analyze abstract specifications of cryptographic protocols against high-level security requirements (such as confidentiality, privacy, and authenticity properties). Despite recent advances in analyzing the implementation code of security protocols [JY05,GP05,BFG06,BFG06a,Gor06,Jur06,Jur07], there are no tools shown to analyze pre-existing protocol implementations in C against high-level security requirements, although tools to check lower-level properties, such as memory safety, do exist. Inventing tools to verify high-level properties of the code—as opposed to abstract specifications—of security protocols is important: in part, because implementation code is often the first and only place where the full details of a protocol are formalized, and in part because even if there is a detailed formal specification, the implementation may introduce additional vulnerabilities. The goal is to start with pre-existing implementations of cryptographic protocols and to verify them against security properties by using formally sound yet practically usable analysis techniques and tools. An important objective is to ensure that these analysis methods are practical by keeping the overhead of their use as small as possible. First, they take input artifacts that are already available in current industrial software development (the program source code). Second, the tools should be reasonably easy to use and have a strong emphasis on automation. Manual effort (such as inserting annotations into the code) should be minimised. The goal of the security analysis is to find code vulnerabilities that give rise to attacks within the Needham-Schroeder threat model (such as man-in-the-middle, replay, or impersonation attacks). The project does not primarily aim to detect buffer-overrun vulnerabilities, as there many existing techniques (including the CCured tool) for detecting or mitigating such problems. Our main aims are to develop a formal security verification methodology to verify implementations of cryptographic protocols in C against security properties, such as confidentiality and authenticity, and to apply the methodology to the implementation of a widely-used security protocol (such as the Internet security protocol standards SSL/TLS, SSH, or Kerberos).

Mohammed Al-LoulahMohammed Al-Loulah 
Dorothy Hodgkin Postgraduate Award
Lancaster University, United Kingdom

Supervisor: Dr. Mike Hazas
Microsoft Research supervisor: James Scott

Research title: Embedded broadband ultrasonic positioning for mobile computing and sensor networks

Research summary: Recent research trends have seen localisation systems move away from a heavy reliance on pre-installed infrastructure, and towards being increasingly embedded and deployable in an ad hoc fashion. However, such embedded implementations lack the robust performance and scalability of their infrastructural counterparts. This proposal argues that sensing over broadband ultrasonic channels is a promising avenue to practical embedded positioning systems. Broadband signalling can provide measurement robustness, vast scalability, and extraction of richer information from positioning signals. Piezopolymer ultrasonic transducers and real-time FPGA embedded signal processing will be combined to create sensor nodes, which will be used to explore and experimentally characterise design aspects such as signal structure, Doppler analysis, array manifolds, and beamforming techniques.

Olle BlombergOlle Blomberg
University of Edinburgh, United Kingdom

Supervisor: Prof. Andy Clark
Microsoft Research supervisor: Richard Harper

Research title: Cognition embodiment and interaction design

Research summary: The cognitive role of body and environment is now a central concern in all of the cognitive sciences. Today, cognitive science is “embodied,” “situated,” and “distributed.” We can refer to this conglomerate of research as Embodied Cognitive Science (ECS). A similar flight has taken place in design-oriented research on how people interact with information technologies. While Human-Computer Interaction (HCI) took off by studying the individual disembodied mind interacting with a desktop computer, the newer field of Computer Supported Cooperative Work (CSCW) is permeated with ethnographic studies of how teams interact with artifacts in organisational environments. Interaction is now “tangible” and computing “ubiquitous,” not just on the desktop. We can refer to this strand of research as Interaction Research (IR). While some researchers have been involved in both ECS and IR, the two flights are not as closely related as one might think. The perspectives that have gained ground in IR mainly come from the social—rather than the cognitive—sciences (for example, ethno-methodology, conversation analysis, and actor-network theory). In ECS, on the other hand, the main thrust—at least originally—came from biologically-inspired works in robotics and artificial life, rather than from naturalistic studies of human beings. Recently, however, the relation between cognition and embodied (social) interaction appears to have become a central issue in both IR and ECS. The aim of the project is to investigate whether, and in which ways, theoretical concepts and empirical findings from ECS and IR can cross-fertilise each other. The aim is not to settle for philosophical clarification but also to propose new concepts and concrete analytical tools that can inform empirical research (in, for example, CSCW). Since IR has developed with largely unexamined assumptions about the nature and role of cognition in interaction, while cognitive science has developed with equally unexamined assumptions about the nature and role of interaction in cognition, both ECS and IR have much to gain from this type of investigation.

Rayna DimitrovaRayna Dimitrova
Saarland University, Germany

Supervisor: Prof. Bernd Finkbeiner
Microsoft Research supervisor: Byron Cook

Research title: Automatic Abstraction for Complex Partial Designs

Shady ElbassuoniShady Elbassuoni
Max Planck Institute for Software Systems, Germany

Supervisor: Prof. Gerhard Weikum
Microsoft Research supervisor: Stephen Robertson

Research title: Language Models for Structured Information Retrieval

The success of knowledge-sharing communities like Wikipedia and the advances in automatic information extraction from textual and Web sources have made it possible to build large “knowledge repositories” such as DBpedia, Freebase, and YAGO. These collections contain structured data that can be viewed as graphs of entities and relationships (ER graphs) or, alternatively, triples in the Semantic-Web data model RDF. Similarly, advanced user intentions can be expressed via structured queries that allow users to explicitly express entities, relationships, and concepts. In such context, queries are typically expressed in the W3C-endorsed SPARQL language or by similarly designed graph-pattern search. However, exact-match query semantics often fall short of satisfying the users' needs by returning too many or too few results. Therefore, IR-style ranking models are crucially needed.

Simon Schubert Simon Schubert
EPFL, Switzerland

Supervisor: Prof. Dejan Kostic
Microsoft Research supervisor: Ant Rowstron

Research title: A framework for overlay bandwidth awareness and allocation

Research summary: The Internet landscape has changed as today’s Internet end-hosts are powerful and well-connected machines. The existing peer-to-peer (P2P) file-sharing applications leverage these capabilities and already consume more than 60 percent of all Internet traffic. With the percentage of broadband connections steadily growing, users are increasingly demanding easy access to entertainment. A new generation of P2P services is started to be deployed on the Internet, characterized as being real-time and high bandwidth, for example real-time video streaming and video-on-demand (VoD) services. These services are more demanding than file download because once the viewing starts, it ideally should not be interrupted. Further, users expect a low latency between starting the application and viewing the media. The hypothesis of this proposal is that the main problem in allocating bandwidth in the existing systems is that there exists an inherent limit to using local decisions in a large-scale system without having any access to global state. In the single overlay case, the problem can manifest itself as degraded, unsatisfactory performance for all nodes. In the case of multiple overlays, the problem materializes as an over-allocation of bandwidth to a lower-priority overlay (for example, in-overlay replication) that can dramatically reduce the performance delivered to what the application deems to be a high-priority overlay (for example, video streaming). In this context, we propose to design and implement a framework for multi-overlay bandwidth awareness and allocation. The key insight behind this proposal is that some amount of global information should be collected in an efficient manner and made available to the system participants. One of our main goals is, therefore, to propose various bandwidth allocation policies and to design, implement, and evaluate mechanisms for enforcing these policies—even in cases of multiple overlays that are competing for the same network bandwidth.

Yana MilevaYana Mileva
Saarland University, Germany

Supervisor: Prof. Andreas Zeller
Microsoft Research supervisor: Brendan Murphy

Research title: Learning from changes

Zartasha MustansarZartasha Mustansar
Dorothy Hodgkin Postgraduate Award 
University of Manchester, United Kingdom

Supervisor: Dr. Lee Margetts
Microsoft Research supervisor: Hillel Kugler

Research title: Extinct but still byte-ing: Using computational biology to bring predatory dinosaurs back to life

Research summary: When talking about dinosaurs in casual conversation, one is usually asked, “How do they know what dinosaurs really looked like?” Today, we are privileged to be able to investigate such questions by using advanced computational biology. The proposed programme of research seeks to use state-of-the-art computational techniques to reverse engineer the walking cycle of a predatory dinosaur. Software for image-based modelling, parallel finite element analysis, and evolutionary robotics will be coupled and deployed over a computational grid comprising many thousands of processors. This resource will facilitate a range of unique meta-experiments, enabling new scientific research to be undertaken that would otherwise not be possible. Not only will these experiments provide insight into the evolution of bipedalism or answer questions such as “How fast could T-Rex run?”, they will also lead to the development of computational techniques that may be applied in classical engineering sectors such as the automotive and aerospace industries.