|
2007 Scholars
 Axel Rack
Freie Universität Berlin, Germany
Supervisor: Prof. Dr Christof Schütte
Microsoft Research contact: Vassily Lyutsarev
Research title:
New mathematical methods for identification of proteins
in mass-spectrometry bases protein profiles
Research summary: Mass spectrometry
(MS) based techniques have emerged as a standard for large-scale protein analysis.
The ongoing progress in terms of more sensitive machines and improved algorithms
led to a constant expansion of its fields of application. Recently, MS was introduced
into clinical proteomics with the prospect of early disease detection using proteomic
pattern matching. MS based characterization and identification of peptides in blood
appears to be one of the arising key technologies for biomarker discovery, understanding
of biological mechanisms, and consequently, it might offer new approaches in drug development.
However, the correct identification (ID) of peptides and proteins
based on MS signals is challenging due to the complexity of the data, which is further amplified
by protein modifications or mutations, cleavage errors, homologous proteins, and sample contamination.
Therefore, the capabilities of standard approaches to efficiently perform an exhaustive ID are limited
and only a small number of known modifications can be considered.
The vastly increased amount of data generated with our sensitive MS
processing pipeline will allow for a greatly improved rate of identified proteins / peptides if
appropriate ID algorithms are available. We think that the application of sophisticated combinatorial
optimization techniques will provide the required means to efficiently perform an exhaustive ID.
This means to be able to include large numbers of modifications as well as additional, biologically
motivated supportive information, such as modification frequency statistics or cleavage statistics.
The project has the following main aims:
-
Development of a sensitive ID algorithm that is able to efficiently cope with big datasets that
integrates reasonably high numbers of protein modifications and other biological side constraints.
-
Integration of this algorithm into the existing MS data processing pipeline to provide a comprehensive
framework for MS based analyses.
-
Development of a web-service based front-end to make the MS data processing pipeline readily available
to a broad range of scientists via the internet.
 Ben Calderhead
University of Glasgow, United Kingdom
Supervisor: Prof. Mark Girolami
Microsoft Research supervisor: Drew Purves
Research title: Bayesian inference in systems biology:
Modelling organ specificity of circadian control in plants
Research summary: Two biological processes in which biochemical
oscillatory behaviour is observed are the cell-cycle and circadian rhythms. Much progress has been made
in the development of mechanistic models to support the study of the underlying biochemical processes
controlling such rhythmic behaviours. Ongoing collaboration between the M Girolami and the laboratory of
Prof. Hugh Nimmo and Prof. Gareth Jenkins (Both from the Plant Molecular Science Group, Division of
Biochemistry and Molecular Biology, Institute of Biomedical and Life Sciences, University of Glasgow)
motivates a highly novel investigation to infer mechanistic models, employing inference methods over
parameters and structure, which will seek to describe the underlying mechanism(s) responsible for tissue
specificity in the circadian control of plant metabolism. The Nimmo Laboratory have made the startling
experimental observation that certain genes within Soybean, and more recently in Arabidopsis Thaliana,
whose expression are under control of the circadian clock, possess the property that the circadian
control is tissue specific. There is currently no detailed definition or adequate model describing the
underlying biochemical mechanism(s) of this phenomenon and there is an immediate need to investigate this
remarkable property. Indeed current mechanistic models of circadian control within plants do not account
for possible communication between different tissues (e.g. leaves and roots) nor do they explain
stimulation of circadian control genes (such as CCA1/LHY) in roots being stimulated by sugars rather
than by light as in shoots. The available experimental data, in the form of time-course microarray gene
expression which the Nimmo Laboratory have produced (and will be producing during the course
of this PhD), presents an outstanding opportunity to systematically, in a hypothesis driven manner,
explore the space of plausible oscillatory control models which provide mechanistic descriptions of the
phenomenon observed.
 Bogdan Ciubotaru
Dublin City University, Ireland
Supervisor: Dr Gabriel-Miro Muntean
Research title: Quality-oriented handover scheme for adaptive multimedia streaming in heterogeneous
wireless networks environment
Research summary: This project aims at proposing a client-server
mechanism employed for quality-oriented multimedia streaming services that monitors current delivery conditions,
analyses network performance, cost and end-user perceived quality parameters and takes decisions in order
to maximize user experience with the service. The decision involves switching from one network to another
and adjusting multimedia content parameters such as resolution and/or frame rate in order to maximize the
end-user perceived quality and to minimize the cost the user has to pay for the streamed multimedia content.
The novel idea is that instead of waiting for the quality to decrease due to either signal power decrease
as the mobile multimedia user reaches network’s maximum range or due to the increase in loss due to
network’s load, the proposed scheme actively finds a better solution.
 Eliot Setzer
University of Edinburgh, United Kingdom
Supervisor: Dr David Aspinall
Microsoft Research supervisor: Georges Gonthier
Research title: Proof engineering: Refactoring proof
Research summary: This is a proposal for research into the
emerging field of *Proof Engineering*, defined to mean the construction, maintenance, and comprehension
of large formal proof developments, by analogy with Software Engineering. Formal proofs, developed and
checked on machine by theorem provers, are important in several application areas. But these applications
are hampered because the proof development process is poorly understood and development tools are seriously
limited. This makes an already difficult activity exceedingly complex, hard to learn, and not as productive
as it could be. For this PhD project, we propose to study theoretically and experimentally implement a
counterpart of refactoring in the domain of proof. Refactoring proofs will allow easier change of design,
and, in particular, experimentation with alternative forms of definitions and theorems.
 Eugenio Giordano
Universitá degli Studi di Bologna, Italy
Supervisor: Prof. Marco Chiani
Microsoft Research supervisor: Ant Rowstron
Research title: Vehicular networks: Safety and beyond. Challenges for the next generation of mobile networks
Research summary: Recent advances in wireless communications and
electronics have enabled the development of low-cost, low-power, multifunctional sensor nodes. The simultaneous
use of several sensor nodes, which include components for sensing, data processing, and communication,
leverage the idea of sensor networks. Indeed, a sensor network is composed of a large number of sensor nodes
that are densely deployed either inside the observed phenomenon or very close to it. This scheme allows
gathering distributed information about any parameter of interest. Nodes participating in a sensor network
could be both, static and mobile, even highly mobile as in the case of vehicular sensor networks (VSNs).
VSNs represent a particular case of sensor networks in which vehicles also embody sensor nodes. Therefore,
vehicles evolve from simple transportation means to moving nodes able to gather data from the surrounding
environment through their embedded sensors and distribute them to other nodes via wireless communications.
This augmented capabilities, coupled with the large number, spread diffusion, and wide mobility range of
vehicles, make them perfectly suited for monitoring factors of public interest such as air pollution level
or temperature. Nevertheless, several traditional and new vehicular contest-related challenges have to be
addressed before making this technology available for the pubic: mobility model tools, routing and topology
control algorithms, and application layer protocols. In this context, few contributions have yet been proposed
to specifically support sensor networking through vehicles. Furthermore VSNs, compared to traditional sensor
networks, present both simplifications ad new challenges. The simplifications can be mainly identified in the
absence of power related issues; the new challenges are related to the high vehicular mobility, high density
of nodes, and absence of supporting infrastructure. The field of study of VSNs includes issues related to
Vehicular Ad Hoc Networks (VANET), wireless sensor networks and delay tolerant networks (DTNs).
 Florian Zuleger
Technical University of Munich, Germany
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.
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.
 Stephen Pike
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.
 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
|
