PhD Summer School 2016

Proving Programs Correct

Abstract

The last few years have seen significant progress in automatic and interactive methods for proving both good properties (such as memory safety) and full functional correctness of computer programs. Recent landmark achievements include the full verification of compilers and operating systems. This talk will cover some of the recent advances in both theory and tools for program verification, and describe some state-of-the-art projects within Microsoft.

Biography

Nick Benton is a Senior Researcher at Microsoft Research in Cambridge, working in the Programming Principles and Tools Group.

Nick’s research ranges from proof theory and categorical logic, through semantics of programming languages and static analyses, to programming language design and compiler implementation. His thesis was on strictness analysis and he has since worked on topics that include term calculi and categorical models for linear logic, MLj and SML.NET (optimizing compilers from SML to the JVM and .NET with extensions for interlanguage working), Polyphonic C#/Cω (C# with join-calculus concurrency and XML/relational data constructs), monads and effect systems, models for dynamic allocation, and, most recently, compositional compiler correctness, mechanically formalized logics for reasoning about machine code programs, and reactive programming.

Nick has a degree in Mathematics and a PhD in Computer Science, both from the University of Cambridge, and is a Fellow Commoner of Queens’ College, where he was previously a Bye-Fellow. Before joining Microsoft, he was an SERC Research Fellow, an RA on an EU ESPRIT project and Senior Research Scientist at Persimmon IT, Inc. Nick has served as Editor-in-Chief of Computer Languages, Systems and Structures (Elsevier) and is currently a member of the Editorial Boards of the Journal of Functional Programming (CUP) and Logical Methods in Computer Science.

The Road to General Artificial Intelligence

Abstract

The creation of machines with human-level, or even super-human, intelligence has long been seen as the ultimate ambition of computer science. New developments in machine learning, coupled with exponential growth in both data and processing power, suggest the time may be ripe to take the next steps towards this elusive goal. In this talk I will highlight some recent progress in this field, and offer some speculative thoughts on potential future directions.

Biography

Chris Bishop is a Microsoft Distinguished Scientist and the Laboratory Director at Microsoft Research Cambridge. He is also Professor of Computer Science at the University of Edinburgh, a Trustee of the Royal Institution (opens in new tab), and a Fellow of Darwin College, Cambridge. In 2004, he was elected Fellow of the Royal Academy of Engineering, and in 2007 he was elected Fellow of the Royal Society of Edinburgh

Chris obtained a BA in Physics from Oxford, and a PhD in Theoretical Physics from the University of Edinburgh, with a thesis on quantum field theory. He then joined Culham Laboratory where he worked on the theory of magnetically confined plasmas as part of the European controlled fusion programme.

From there, he developed an interest in pattern recognition, and became Head of the Applied Neurocomputing Centre at AEA Technology. He was subsequently elected to a Chair in the Department of Computer Science and Applied Mathematics at Aston University, where he led the Neural Computing Research Group. Chris then took a sabbatical during which time he was principal organiser of the six month international research programme on Neural Networks and Machine Learning at the Isaac Newton Institute for Mathematical Sciences in Cambridge, which ran in 1997.

After completion of the Newton Institute programme Chris joined the Microsoft Research Laboratory in Cambridge.

No Compromises: Distributed Transactions with Consistency, Availability, and Performance

Abstract

Transactions with strong consistency and high availability simplify building and reasoning about distributed systems. However, previous implementations performed poorly. This forced system designers to avoid transactions completely, to weaken consistency guarantees, or to provide single machine transactions that require programmers to partition their data. In this paper, we show that there is no need to compromise in modern data centers. We show that a main memory distributed computing platform called FaRM can provide distributed transactions with strict serializability, high performance, durability, and high availability. FaRM achieves a peak throughput of 140 million TATP transactions per second on 90 machines with a 4.9 TB database, and it recovers from a failure in less than 50 ms. Key to achieving these results was the design of new transaction, replication, and recovery protocols from first principles to leverage commodity networks with RDMA and a new, inexpensive approach to providing non-volatile DRAM.

Biography

I work as a researcher in Systems and Networking group at MSR Cambridge. My main interest is building scalable parallel and distributed systems. I prefer staying on the practical side of problems and enjoy implementing real systems ranging from simple script based solutions to everyday problems to complex production systems. Lately I have been really excited about several emerging hardware trends and their impact on the design of software systems that run in data centres. Three major trends really stand out: large main memories of modern machines, very fast networks and interconnects, and increasingly higher integration of components on chips. Common to all these trends is how they enable building much denser computers, meaning that performing the same computation on the same amount of data requires much less space and is cheaper than with traditional hardware. I am mostly interested in how these novel hardware developments impact software, as we need to change the software stacks, from the operating and runtime systems to the applications, in order to best utilize them. . I received my PhD from EPFL Switzerland in 2012, where I worked on performance of software transactional memory. Before that, I received my Graduate Electrical Engineer diploma from University of Novi Sad, Serbia in 2004.

Reprogramming Cells: How can we edit Biological Programs

Abstract

In the context of stem cell biology, ‘reprogramming’ is a term that refers to the process of inducing an adult cell, such as one of your skin cells, back to the most naïve, stem-like state. This was a Nobel Prize winning feat achieved first in 2006 by Japanese scientist, Shinya Yamanaka. Since his pioneering work, reprogramming to induced pluripotency – a term that refers to the ability of these cells to generate all adult cell types – has been demonstrated from a diverse range of cells. However, the efficiency of the process is very limited, and we do not yet have an understanding of the mechanism that governs conversion. This talk will approach this problem from the perspective of the biological program that governs decision-making in stem cells. In possession of an explanation of the information processing carried out by these cells, we can unpack the sequence of molecular events that must occur during successful reprogramming, identify bottlenecks in the process and ultimately use this understanding to predict how to edit the program to drive the process with high efficiency. Such understanding is key as we seek to derive patient-specific pluripotent cells that can be used in cell therapies and regenerative medicine.

Biography

Sara-Jane Dunn is a Scientist in the Biological Computation group at Microsoft Research, Cambridge. She studied Mathematics at the University of Oxford, graduating with a MMath in 2007. She remained in Oxford for postgraduate study as a student of the Life Sciences Interface Doctoral Training Centre, completing an intensive training course in the application of mathematical, physical, computational and engineering science techniques to the biomedical and life sciences. At the end of 2008, she joined the Computational Biology group at the Department of Computer Science to begin her DPhil research. Subsequently, in 2012, she joined Microsoft Research as a postdoctoral researcher in Biological Computation, before transitioning to a permanent Scientist position in 2014. In 2016 she was invited to become an Affiliate Research of the Wellcome Trust-Medical Research Council Stem Cell Institute, University of Cambridge. Her research focuses on uncovering the fundamental principles of biological information-processing, with a particular focus on decision-making in Development.

How to Present a Poster at an International Conference

Abstract

Presenting a poster at an international conference is a terrific opportunity to promote your research and raise your professional profile in a global academic forum. However, it can be daunting to compete with other presenters to get the attention of a passing audience. As well as a clear and captivating poster, you need the ability to build rapport quickly and present your subject positively and succinctly.

This can be especially challenging when English is the shared language but not everyone’s mother tongue. Whether you are a native or a non-native English speaker, you will require flexibility and sensitivity to others in order to communicate effectively.

During the three poster sessions, Sue will be hovering in the room, watching and listening to your approach. She will then highlight on the final day the key thought-processes as well as the verbal and non-verbal skills needed to present a poster successfully.

Sue will also be available each day to provide confidential one-to-one feedback for any students who sign up.

Biography

Sue Duraikan runs Duraikan Training (www.duraikan-training.com (opens in new tab)), a consultancy which aims to help individuals and organisations develop. We provide support in designing and delivering learning strategies. We also run group workshops and one-to-one coaching on a wide range of professional skills. As a former teacher of French and German and with wide experience of working globally, Sue has a particular interest in cross-cultural communication, and deep respect for those who operate daily in a second or third language.

Strategic Thinking for Researchers

Abstract

From time to time at Microsoft Research, we set aside time to talk about strategic aspects of research, that is, the big picture of why we do research and how to have different sorts of impact, beyond the more immediate tasks of writing papers, giving talks, and transferring ideas. This talk will cover some of these strategies for having a happy and productive career as a researcher.

Biography

Andy Gordon is a principal researcher at Microsoft Research Cambridge, where he manages Programming Principles and Tools, and is a Professor at the University of Edinburgh. Andy wrote his PhD on input/output in lazy functional programming, and is the proud inventor of Haskell’s “>>=” notation for monads. He’s worked on a range of topics in concurrency, verification, and security, never straying too far from his roots in functional programming. His current passion is a functional language to enable probabilistic inference from Excel.

Project Malmo – a platform for fundamental AI research

Abstract

I present Project Malmo – an AI experimentation platform built on top of the popular computer game Minecraft, and designed to support fundamental research in artificial intelligence. As the AI research community pushes for artificial general intelligence (AGI), experimentation platforms are needed that support the development of flexible agents that learn to solve diverse tasks in complex environments. Minecraft is an ideal foundation for such a platform, as it exposes agents to complex 3D worlds, coupled with infinitely varied game-play.

Project Malmo provides a sophisticated abstraction layer on top of Minecraft that supports a wide range of experimentation scenarios, ranging from navigation and survival to collaboration and problem solving tasks. In this talk I discuss Malmo, and how it can push help the research community tackle the next big challenges in AI.

Biography

Katja Hofmann is a researcher at Microsoft Research Cambridge. As part of the Machine Intelligence and Perception group, she is research lead of Project Malmo. Before joining Microsoft Research, Katja received her PhD in Computer Science from the University of Amsterdam, her MSc in Computer Science from California State University, and her BSc in Computer Science from the University of Applied Sciences in Dresden, Germany. Katja’s main research goal is to develop interactive learning systems. Her dream is to develop AIs that learn to collaborate with human players in Minecraft.

The Evolution of Innovation

Abstract

Innovation has been at the heart of human progress for centuries. The nature and pace of innovation, however, has changed dramatically over time. Hermann Hauser’s talk will start with a survey of innovation since the invention of the wheel and end with remarks on the latest advances in machine leaning and artificial intelligence. The increased speed of these advances makes it necessary to take a more pro active approach to societal and ethical issues in an expected era of Superintelligences.

Biography

In 2015, Hermann was awarded a KBE for services to Engineering and Industry.

Serial entrepreneur and co-founder of Amadeus Capital Partners, Dr Hermann Hauser CBE has wide experience in developing and financing companies in the information technology sector. He co-founded a number of high-tech companies including Acorn Computers which spun out ARM, E-trade UK, Virata and Cambridge Network. Subsequently, Hermann became vice president of research at Olivetti. During his tenure at Olivetti, he established a global network of research laboratories. Since leaving Olivetti, Hermann has founded over 20 technology companies. In 1997, he co-founded Amadeus Capital Partners. At Amadeus, he invested in CSR, Solexa, Icera, Xmos and Cambridge Broadband.

Hermann is a Fellow of the Royal Society, the Institute of Physics and of the Royal Academy of Engineering and an Honorary Fellow of King’s College, Cambridge. In 2001, he was awarded an Honorary CBE for ‘innovative service to the UK enterprise sector’. In 2004, he was made a member of the Government’s Council for Science and Technology and in 2013, he was made a Distinguished Fellow of BCS, the Chartered Institute for IT.

Hermann has honorary doctorates from the Universities of Loughborough, Bath, Anglia Ruskin and The University of Strathclyde.

Improving Reliability of Compilers

Abstract

Compilers are at the bottom of the software stack: every program produced today has to go through at least one compiler. Therefore the reliability, security, and performance of the entire software ecosystem depends on compilers functioning properly.

However, modern compilers consist of several million lines of code. Like any large piece of software, compilers are also encumbered with bugs. Compiler bugs vary from simple crashes to introducing changes in behavior in compiled programs or introducing security vulnerabilities in said programs.

In this talk I’ll present techniques for increasing reliability of compilers through automated verification.

Biography

Nuno Lopes is a researcher at MSR Cambridge. He holds a PhD from the University of Lisbon, and has previously interned at MSR Redmond, Apple’s compiler team, Max Planck Institute (MPI-SWS), and the Institute for Systems and Robotics Lisbon.

Nuno’s research interests include software verification, compilers, and mixing the two.

Ultra Sound Innovations

Abstract

Ultrasound imaging is being revolutionized by advances in consumer electronics which means portable devices are becoming widely available at reducing cost. The main barrier to wider application today is the skill required to acquire and interpret diagnostic data.

I will describe our inter-disciplinary efforts towards making ultrasound an easier technology to use by a non-expert. Some of this work is inspired by advances in machine learning in computer vision. Challenges relate in part to how to automate detection and diagnostic measurement in data of variable quality typical of real world clinical use, but perhaps more scientifically interesting, how to design computer algorithms that can recover biomarkers hidden within acoustic patterns that are difficult to perceive by the radiologists eye.

Biography

Alison is the Technikos Professor of Biomedical Engineering at the University of Oxford. Her university research group is internationally known for its work on biomedical image analysis, and in particular ultrasound image analysis and inter-disciplinary application of the technology in the developed and developing world. She was the recipient of the inaugural IFMBE Laura Bassi award in 2015 and a European Research Council (ERC) Advanced Grant in 2016.

Alison is currently, or has been, a member of numerous RCUK, Royal Academy of Engineering and Royal Society strategic and policy making committees and grant awarding panels. She is the former President of the MICCAI Society, the international society in her field, and has recently been elected to the Board of Trustees of the Institution of Engineering and Technology (IET).

She received an OBE for services to science and engineering in 2013.

Towards Trusted Cloud

Abstract

This talk will focus on the research efforts surrounding the Trusted Cloud (opens in new tab) project at Microsoft Research. The Trusted Cloud aims to provide customers of cloud computing complete control over their data: no one, including malicious employees and hackers, should be able to access the data without the customer’s permission. As a first and essential step towards our goal, we propose to isolate customers’ workloads and reduce the trusted computing base within the cloud environment. We do so with the help of secure hardware (for example, Intel SGX) or small trusted hypervisors.

Though the above step reduces the attack surface significantly, we wish to protect customer’s workloads even further. We observe that the interaction of customer’s code with untrusted environment via accesses to memory, disk and network can leak confidential information. To this end, we propose data-oblivious techniques that obfuscate real accesses of the code from an adversary who observes the memory traffic. I will describe in detail our approach of designing general data structures and algorithms, such as oblivious RAM and data-oblivious shuffle, and specialised techniques for MapReduce and machine learning algorithms.

Biography

Olya Ohrimenko is a researcher in Constructive Security Group at Microsoft Research, Cambridge, and a research fellow at Darwin College, Cambridge University. Her research interests include privacy, integrity and security issues that emerge in the cloud computing environment. Olya received her Ph.D. degree from Brown University in 2013 and a B.CS. (Hons) degree from The University of Melbourne in 2007. She was an intern at Google, Microsoft Research Redmond and IBM Research Zurich.

How to Write a Great Research Paper & How to Give a Great Research Talk

Research paper slides PDF (opens in new tab) | Research talk slides PDF (opens in new tab)

Abstract

Writing papers and giving talks are key skills for any researcher, but they aren’t easy. In this pair of presentations, I’ll describe simple guidelines that I follow for writing papers and giving talks, which I think may be useful to you too. I don’t have all the answers-far from it-so I hope that the presentation will evolve into a discussion in which you share your own insights, rather than a lecture.

Biography

Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research in 1998. His main research interest is in functional programming languages, their implementation, and their application. He has led a succession of research projects focused around the design and implementation of production-quality functional-language systems for both uniprocessors and parallel machines. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages. More generally, he is interested in language design, rich type systems, software component architectures, compiler technology, code generation, runtime systems, virtual machines, garbage collection, and more. He is particularly motivated by direct use of principled theory to practical language design and implementation-that’s one reason he loves functional programming so much. He is also keen to apply ideas from advanced programming languages to mainstream settings.

When Distortion is Good and Fidelity is Bad: Lessons from Video-mediated Communication Research in the Wild

Abstract

Video-mediated communication is often assumed to be ‘the next best thing to being there’. However, despite its long commercial and research history there is still many puzzles about what users will treat as comfortable. Using examples from field research into couples coping with distortion in video calling and news users trying out video messaging, this talk will unpack some counter-intuitive findings about what users value about communicative richness. While technology frames human communication, it does not determine the course or outcomes, rather its material effects on communication are treated by end users as resources for social meaning. This talk will argue that the real measure of communicative richness is perceived flexibility of the control of meaning. Designing new communication technologies thus requires leveraging the innate flexibility of meaning in human communication rather than assuming that communication takes care of itself after a certain threshold of fidelity is achieved.

Biography

Sean Rintel is a Researcher in the Human Experience and Design (HXD) group at MSRC. His research explores how the affordances of technologies mediate language, social action, and culture. He has written about technologized communication in contexts such as video calling and video messaging in personal relationships, Internet Relay Chat openings and non-responses, Facebook in the workplace, crisis memes, the mediatization of politics in social media, and social media error messages. He is the Senior Editor for Communication Technology in new online Oxford Research Encyclopaedia of Communication project.

Summer School Chair; Welcome to PhD Summer School 2016

Biography

Scarlet Schwiderski-Grosche is a Senior Research Program Manager at Microsoft Research Cambridge, working for Microsoft Research Outreach in the Europe, Middle East, and Africa (EMEA) region. She is responsible for academic research partnerships in the region, especially for the Joint Research Centres with Inria in France and EPFL and ETH Zurich in Switzerland.

Scarlet has a PhD in Computer Science from University of Cambridge. She was in academia for almost 10 years before joining Microsoft in March 2009. In academia, she worked as Lecturer in Information Security at Royal Holloway, University of London.

The Future of Interaction in Augmented and Virtual Reality

Biography

Jamie Shotton leads the Machine Intelligence & Perception group at Microsoft Research Cambridge.  He studied Computer Science at the University of Cambridge, where he remained for his PhD in computer vision and machine learning for visual object recognition. He joined Microsoft Research in 2008 where he is now a Principal Researcher. His research focuses at the intersection of computer vision, AI, machine learning, and graphics, with particular emphasis on systems that allow people to interact naturally with computers. He has received multiple Best Paper and Best Demo awards at top academic conferences. His work on machine learning for body part recognition for Kinect was awarded the Royal Academy of Engineering’s gold medal MacRobert Award 2011, and he shares Microsoft’s Outstanding Technical Achievement Award for 2012 with the Kinect engineering team. In 2014 he received the PAMI Young Researcher Award, and in 2015 the MIT Technology Review Innovator Under 35 Award (“TR35”).

Accelerate Your Research with Microsoft Azure

Biography

Dr Kenji Takeda is Solutions Architect and Technical Manager for the Microsoft Research Outreach EMEA team. He has extensive experience in Cloud Computing, High Performance and High Productivity Computing, Data-intensive Science, Scientific Workflows, Scholarly Communication, Engineering and Educational Outreach. He has a passion for developing novel computational approaches to tackle fundamental and applied problems in science and engineering. He was previously Co-Director of the Microsoft Institute for High Performance Computing, and Senior Lecturer in Aeronautics, at the University of Southampton, UK. There he worked with leading high value manufacturing companies such as Airbus, AgustaWestland, BAE Systems, Rolls-Royce and Formula One teams, to develop state-of-the-art capability for improving science and engineering processes. He also worked in the areas of aerodynamics, aeroacoustics and flight simulation.

Delivering a Fabulous Research Talk: How to Tell More Stories, Use Less PowerPoint and Get to the Point When Presenting

Abstract

We’ve all been there: a dark room, a long and boring speech accompanied by an endless stream of bullet-heavy PowerPoint slides. It’s maddening. In this session you’ll learn how to really engage an audience, how to deliver a research presentation with emphasis and energy, and finally how to use body language to your advantage. You’ll also learn what separates a good presentation slide from a bad one, and how to calibrate a speech so that even complicated, technical topics can be explained in a clear, concise, compelling way.

Biography

Dave is a strategic communications expert with more than 19 years of experience in the field. A former newspaper reporter and columnist, Dave has counseled senior executives at a variety of companies, managed communications teams and led business development efforts. He has also conducted storytelling workshops and presentation training sessions for thousands of executives at numerous companies, including Microsoft, CA, Clif Bar, Dell, CBS, Ingram Micro, aQuantive, T-Mobile, MercyCorps, DriveSavers, Reebok, Tripwire, Wieden + Kennedy, SnapChat, Zurich Insurance, and Adidas.

He has spoken to numerous groups about how to translate complex scientific and technical information into clear, concise, compelling language. Before establishing Elevator Speech Inc., Dave was the general manager of Weber Shandwick’s Portland office. Before joining Weber Shandwick, he led a Waggener Edstrom PR team charged with developing strategic PR programs for Microsoft in a variety of industries, including financial services, manufacturing and healthcare. Dave was an award- winning reporter and columnist at The Galveston Daily News in Texas and an on-camera spokesman for The University of Texas Medical Branch. He is a graduate of the University of Northern Colorado’s school of journalism.

Innovation, Invention & Design Thinking

Abstract

A look at the tools and methods of design thinking and how these approach innovation and technology invention. Focusing on processes & case-studies in user-centered design, crowdsourcing, technology-driven invention.

Biography

Haiyan Zhang (opens in new tab) is a designer, technologist and maker of things.

She is Innovation Director at Microsoft Research Cambridge. Inventing cutting-edge technology to enable new “Connected Play” experiences. Currently filming a documentary for BBC2 on design and invention in the UK.

Haiyan was formerly Innovation Director at Lift London, a Microsoft Game Studio; Co-Founder and Design Lead for the innovation platform, OpenIDEO. With over 50,000 users worldwide solving challenges for social good and used as the enterprise innovation engine for organisations such as British Airways, DeutscheBank, Harvard Business School.

Working at the design consultancy, IDEO, she has created innovative tech experiences for community building, entertainment, financial services. She has worked with leading video game makers on research and ideas for new play experiences. Clients have included Mattel, Electronic Arts, HBO, France Telecom, Alcatel, Cisco, and AT&T.

Haiyan believes in a holistic approach to design. Starting from user research and insights, she leverages her design skills to create prototypes, interfaces, sketches, scenarios, advertisements to reflect the user’s experience as a journey beyond a single product moment.

Haiyan’s work is informed by her previous profession as a software engineer and user interface designer creating applications for the biomedical and data-mining industries. As part of a team of software developers from Excel Tech in Canada, she created an electroencephalograph (EEG) visualization tool for intra-operative monitoring which is currently being used in hospitals across North America.

Haiyan graduated in 2006 with distinction in a Masters degree in Interaction Design from the renowned Interaction Design Institute in Ivrea, and has a Bachelor of Computer Science (First-Class Honours) from Monash University, Australia.

She has lived and worked in Australia, Toronto, China, Italy, San Francisco and now resides in London.