Microsoft Research is the research subsidiary of Microsoft. It was formed in 1991, with the intent to advance state-of-the-art computing and solve difficult world problems through technological innovation in collaboration with academic, government, and industry researchers. The Microsoft Research team employs more than 1,000 computer scientists, physicists, engineers, and mathematicians, including Turing Award winners, Fields Medal winners, MacArthur Fellows, and Dijkstra Prize winners.
Between 2010 and 2018, 154,000 AI patents were filed worldwide, with Microsoft having by far the largest percentage of those patents, at 20%.
Microsoft Research includes the core Microsoft Research labs and Microsoft Research AI, directed by Technical Fellow Eric Horvitz, and Microsoft Research NeXT (for New Experiences and Technologies), directed by corporate vice president Peter Lee.
Microsoft research is categorized into the following broad areas:
Microsoft Research sponsors the Microsoft Research Fellowship for graduate students.
Microsoft has research labs around the world:
Microsoft Research invests in multi-year collaborative joint research with academic institutions at Barcelona Supercomputing Center, INRIA, Carnegie Mellon University, Massachusetts Institute of Technology, Sao Paulo Research Foundation (FAPESP), the Microsoft Research Centre for Social NUI and others.
The Association for Women in Mathematics (AWM) is a professional society whose mission is to encourage women and girls to study and to have active careers in the mathematical sciences, and to promote equal opportunity for and the equal treatment of women and girls in the mathematical sciences. The AWM was founded in 1971 and incorporated in the state of Massachusetts. AWM has approximately 5200 members, including over 250 institutional members, such as colleges, universities, institutes, and mathematical societies. It offers numerous programs and workshops to mentor women and girls in the mathematical sciences. Much of AWM’s work is supported through federal grants.Bigtop (Microsoft product)
Bigtop is a Microsoft Research project which gives a framework to create a set of loosely coupled distributed system components. This will result in the creation of a Grid Operating system. Bigtop is not expected before the end of this decade. It is not clear whether Bigtop will be integrated into Windows or launched as a different operating system.Cω
Cω (pronounced "see omega"; usually written "Cw" or "Comega" whenever the "ω" symbol is not available) is a free extension to the C# programming language, developed by the WebData team in Microsoft SQL Server in collaboration with Microsoft Research in the UK and Redmond. It was formerly known as the codenames X# (X Sharp) and Xen. It was renamed Cω after Polyphonic C#, another research language based on the join calculus, was integrated into it.Dryad (programming)
Dryad was a research project at Microsoft Research for a general purpose runtime for execution of data parallel applications. Microsoft made several preview releases of this technology available as add-ons to Windows HPC Server 2008 R2. However, in October 2011, Microsoft discontinued active development on Dryad, shifting focus to the Apache Hadoop framework.An application written for Dryad is modeled as a directed acyclic graph (DAG). The DAG defines the dataflow of the application, and the vertices of the graph defines the operations that are to be performed on the data. The "computational vertices" are written using sequential constructs, devoid of any concurrency or mutual exclusion semantics. The Dryad runtime parallelizes the dataflow graph by distributing the computational vertices across various execution engines (which can be multiple processor cores on the same computer or different physical computers connected by a network, as in a cluster). Scheduling of the computational vertices on the available hardware is handled by the Dryad runtime, without any explicit intervention by the developer of the application or administrator of the network. The flow of data between one computational vertex to another is implemented by using communication "channels" between the vertices, which in physical implementation is realized by TCP/IP streams, shared memory or temporary files. A stream is used at runtime to transport a finite number of structured Items.
Dryad defines a domain-specific language, which is implemented via a C++ library, that is used to create and model a Dryad execution graph. Computational vertices are written using standard C++ constructs. To make them accessible to the Dryad runtime, they must be encapsulated in a class that inherits from the GraphNode base class. The graph is defined by adding edges; edges are added by using a composition operator (defined by Dryad) that connects two graphs (or two nodes of a graph) with an edge. Managed code wrappers for the Dryad API can also be written.
There exist several high-level language compilers which use Dryad as a runtime; examples include Scope (Structured Computations Optimized for Parallel Execution) and DryadLINQ.Gazelle (web browser)
Gazelle was a research web browser project by Microsoft Research, first announced in early 2009. The central notion of the project was to apply operating system (OS) principles to browser construction. In particular, the browser had a secure kernel, modelled after an OS kernel, and various web sources run as separate "principals" above that, similar to user space processes in an OS. The goal of doing this was to prevent bad code from one web source to affect the rendering or processing of code from other web sources. Browser plugins are also managed as principals.Gazelle had a predecessor project, MashupOS, but with Gazelle the emphasis was on a more secure browser.By the July 2009 announcement of Google Chrome OS, Gazelle was seen as a possible alternative Microsoft architectural approach compared to Google's direction. That is, rather than the OS being reduced in role to that of a browser, the browser would be strengthened using OS principles.The Gazelle project became dormant, and ServiceOS arose as a replacement project also related to browser architectures. But by 2015, the SecureOS project was also dormant, after Microsoft decided that its new flagship browser would be Edge.Harry Shum
Heung-Yeung "Harry" Shum (Chinese: 沈向洋; born in October 1966) is a computer scientist of Chinese origin. He is the Executive Vice President of Artificial Intelligence & Research at Microsoft. He is known for his research on computer vision and computer graphics, and for the development of the search engine Bing.HomeOS
HomeOS is the working title of a home automation operating system that was being developed at Microsoft Research in the early 2010s. Microsoft Research announced the project in 2010.
HomeOS communicates with Lab of Things, a cloud-based Internet of Things infrastructure also developed by Microsoft.The slogan for the HomeOS project is "Enabling smarter homes for everyone."The HomeOS development team has written three sample applications that make use of multiple devices, including a "sticky media" app that plays music in parts of the house that are lit up, but not other rooms; a two-factor authentication app that uses audio from smartphones and images from a front-door camera to turn on lights when a user is identified; and a home browser for viewing and controlling a user's access to all devices in a home.Some staff who worked on the HomeOS project cited Microsoft CEO Steve Ballmer's focus on enterprise applications, productivity software, and cloud computing as the reason for the stalled development of HomeOS.Jennifer Tour Chayes
Jennifer Tour Chayes is a Technical Fellow and Managing Director of Microsoft Research New England in Cambridge, Massachusetts, which she founded in 2008, and Microsoft Research New York City, which she founded in 2012. Chayes is best known for her work on phase transitions in discrete mathematics and computer science, structural and dynamical properties of self-engineered networks, and algorithmic game theory. She is considered one of the world's experts in the modeling and analysis of dynamically growing graphs. Chayes has been with Microsoft Research since 1997, when she co-founded the Theory Group. She received her Ph.D. in mathematical physics at Princeton University in 1983. She is Affiliate Professor of Mathematics and Physics at the University of Washington, and was for many years Professor of Mathematics at UCLA. She is an author on almost 120 scientific papers and the inventor on more than 25 patents.Microsoft Academic
Microsoft Academic is a free public web search engine for academic publications and literature, developed by Microsoft Research. Re-launched in 2016, the tool features an entirely new data structure and search engine using semantic search technologies. It currently indexes over 220 million publications, 88 million of which are journal articles. The Academic Knowledge API offers information retrieval from the underlying database using REST endpoints for advanced research purposes.The service replaces the earlier Microsoft research project, Microsoft Academic Search, which ended development in 2012.Preliminary reviews by bibliometricians suggest the new Microsoft Academic Search is a competitor to Google Scholar, Web of Science, and Scopus for academic research purposes as well as citation analysis.Microsoft Academic Search
Microsoft Academic Search was a research project and academic search engine retired in 2012. It relaunched in 2016 as Microsoft Academic.Microsoft Comic Chat
Microsoft Comic Chat (later Microsoft Chat, but not to be confused with Windows Chat, or WinChat) is a graphical IRC client created by Microsoft, first released with Internet Explorer 3.0 in 1996. Comic Chat was developed by Microsoft Researcher David Kurlander, with Microsoft Research's Virtual Worlds Group and later a group he managed in Microsoft's Internet Division.Microsoft Research Maps
Microsoft Research Maps or MSR Maps was a free online repository of public domain aerial imagery and topographic maps provided by the U.S. Geological Survey (USGS). The site was a collaboration between Microsoft Research (MSR), Bing Maps, and the USGS. It had been in operation since June 1998. It had 30,000 to 50,000 visitors per day as of January 2010. The site was renamed in 2010, prior to which it had been known as TerraServer-USA (formerly Microsoft TerraServer).
The site had black and white USGS aerial photographs of approximately 97% of the United States. In 2000, the USGS launched the new Urban Areas program, which will ultimately take high-resolution color aerial photographs of about 100 major American cities. MSR Maps had Urban Areas data for 40 cities.Microsoft had announced that the MSR Maps web site was going to permanently close on May 1, 2012, but later changed that decision based on requests from users of the site. As of March 2016 the site is no longer available.Midori (operating system)
Midori was the code name for a managed code operating system being developed by Microsoft with joint effort of Microsoft Research. It had been reported to be a possible commercial implementation of the Singularity operating system, a research project started in 2003 to build a highly dependable operating system in which the kernel, device drivers, and applications are all written in managed code. It was designed for concurrency, and could run a program spread across multiple nodes at once. It also featured a security model that sandboxes applications for increased security. Microsoft had mapped out several possible migration paths from Windows to Midori. The operating system was discontinued some time in 2015, though many of its concepts were rolled into other Microsoft projects.Richard Rashid
Richard Ferris Rashid served as a VP at Microsoft for many years. He oversaw Microsoft Research's worldwide operations until 2012. Previously, he was the director of Microsoft Research. He joined Microsoft Research in 1991, and was promoted to vice president in 1994. In 2000, he became senior vice president. He has authored a number of patents in areas such as data compression, networking, and operating systems, and was a major developer of Microsoft's interactive TV system.
Rashid graduated from Stanford University in 1974 with degrees in mathematics and comparative literature. He then received a Master of Science and a Ph.D. in computer science from the University of Rochester, finishing in 1980. While at Rochester, he and Gene Ball wrote what is probably one of the earliest networked multiplayer computer games, Alto Trek, for Xerox Alto computers.
In 1979, he became a professor of computer science at Carnegie Mellon University. While a faculty member, he performed research and published numerous papers and articles on topics such as networking, operating systems, artificial intelligence, and programming languages for distributed computing applications. His most notable work was on the Mach kernel.Singularity (operating system)
Singularity is an experimental operating system (OS) which was built by Microsoft Research between 2003 and 2010. It was designed as a high dependability OS in which the kernel, device drivers, and application software were all written in managed code. Internal security uses type safety instead of hardware memory protection.So.cl
So.cl (pronounced "social") was a social networking service and social search engine operated by Microsoft FUSE Labs. Microsoft FUSE Labs announced on March 7, 2017 that it would be closing down So.cl on March 15, 2017.Spec Sharp
Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions. Like ESC/Java, it includes a static checking tool based on a theorem prover that is able to statically verify many of these invariants. It also includes a variety of other minor extensions to the language, such as non-null reference types.
The code contracts API in the .NET Framework 4.0 has evolved with Spec#.
Microsoft Research developed both Spec# and C#; in turn, Spec# serves as the foundation of the Sing# programming language, which Microsoft Research also developed.Venkata Padmanabhan
Venkata Narayana Padmanabhan is a computer scientist and principal researcher at Microsoft Research India. He is known for his research in networked and mobile systems. He is an elected fellow of the Indian National Academy of Engineering, Institute of Electrical and Electronics Engineers and the Association for Computing Machinery. The Council of Scientific and Industrial Research, the apex agency of the Government of India for scientific research, awarded him the Shanti Swarup Bhatnagar Prize for Science and Technology, one of the highest Indian science awards for his contributions to Engineering Sciences in 2016.Verve (operating system)
Verve is a research operating system developed by Microsoft Research. Verve is verified end-to-end for type safety and memory safety.
Because of their complexity, a holy grail of software verification has been to verify properties of operating systems. Operating systems are usually written in low-level languages, such as C, that provide very few guarantees. The Singularity project took the approach of writing an operating system in C#, a type-safe, memory-safe language. A weakness of this approach is that operating systems necessarily need to call lower-level code to, for instance, move the stack pointer. Verve addresses this problem by partitioning the operating system into verified assembly that is required to be low-level and a trusted interface to rest of the operating system, written in C#. There is a trusted specification that guarantees the low-level assembly code does not mess with the heap and that the high-level C# code does not mess with the stacks.
Verve consists of a small Nucleus, which acts as a minimal hardware abstraction layer, and a Kernel, which uses primitives provided by the Nucleus to expose a more traditional interface to applications. All components of the system other than the Nucleus are written in managed C# and compiled by Bartok (originally developed for the Singularity project) into typed assembly language, which is verified by a TAL checker.
The Nucleus implements a memory allocator and garbage collection, support for stack switching, and managing interrupt handlers.
It is written in BoogiePL, which serves as input to MSR's Boogie verifier, which proves the Nucleus correct using the Z3 SMT solver. The Nucleus relies on the Kernel to implement threads, scheduling, synchronization, and to provide most interrupt handlers. Even though the Kernel is not formally verified, so, for example, a bug in scheduling could cause the system to hang, it cannot violate type or memory safety, and thus cannot directly cause undefined behavior. If it attempts to make invalid requests to the Nucleus, formal verification guarantees that the Nucleus handles the situation in a controlled manner.
Verve's trusted computing base is limited to: Boogie/Z3 for verifying the Nucleus's correctness; BoogieASM for translating it into x86 assembly; the BoogiePL specification of how the Nucleus should behave; the TAL verifier; the assembler and linker; and the bootloader. Notably, neither the C# compiler/runtime nor the Bartok compiler are part of the TCB.
Microsoft Research (MSR)