We are designing programming languages for building safe and reliable asynchronous systems. The languages are based on the programming idiom of communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of code. They offer systematic testing capabilities that exhaustively (in the limit) tests all possible executions of the program, weeding out even hard-to-find concurrency bugs.
IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness. It also provides a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Uncertainty is a C# library that uses LINQ to let developers easily express probabilistic computations and then inference over those computations. See our recorded Research In Focus talk from the Microsoft Faculty Summit (http://research.microsoft.com/apps/video/?id=251861) this past year for more information. Uncertain
Mobius (formerly known as Spark-CLR) is an cross-company open source project to provide C# language bindings for Apache Spark, which is a cluster computing framework built around the core programming abstractions of Resilient Distributed Datasets (RDDs), a logical collection of data partitioned across machines, and Discretized Streams (DStreams), a temporal sequence of RDDs.
Open source is a powerful way to advance software development and share data for experimentation. Microsoft has research projects as well as key software—such as .NET—in open-source repositories. These tools provide opportunities for engaging with Microsoft researchers and advancing the state of the art together. The powerful software can be used in classes and projects to prepare students for real-world applications.
The BBC and partners, including Microsoft, announce the BBC micro:bit – a pocket-sized, codeable computer that allows children to get creative with technology. Up to 1 million micro:bits will be given to every 11 or 12 year old child in Year 7 or equivalent across the UK, for free.
Robust Distributed System Nucleus (rDSN) is an open framework for quickly building and managing high performance and robust distributed systems. The core idea is a coherent and principled design that distributed systems, tools, and frameworks can be developed independently and later on integrated (almost) transparently.
Logic flaws are prevalent in multiparty cloud services, which cause serious consequences, e.g., an attacker can make purchases without paying, or gets into other people’s accounts without password. For decades, researchers have been advocating formal verification as a solution, but in the real world developers face many major hurdles to do it. We introduce a technology that significantly lowers these hurdles, and show its effectiveness in real-world deployments.
We envision a future Internet of Things where every human-created artifact in the world that uses electricity will be connected to the internet. We are creating new experiences and technologies for the coming convergence of digital and physical systems enabled in this future.
Code Hunt is a serious educational game. The Code Hunt community is interested in all aspects of research and development around the game, including analysis of the data and development of the platform.
Code Hunt is a serious gaming platform for coding contests and practicing programming skills. It is based on the symbolic white box execution engine, Pex. Code Hunt is unique as an online coding platform in that each puzzle is presented with test cases only, no specification. Players have to first work out the pattern and then code the answer. Code Hunt has been used by over 100,000 players as of February 2015.
Parasail is a novel approach to parallelizing a large class of seemingly sequential applications wherein dependencies are, at runtime, treated as symbolic values. The efficiency of parallelization, then, depends on the efficiency of the symbolic computation, an active area of research in static analysis, verification, and partial evaluation. This is exciting as advances in these fields can translate to novel parallel algorithms for sequential computation.
An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times.
an overhead-constraint logging system
Software-defined radios (SDR) have a potential to bring major innovation in wireless networking design. However, their impact so far has been limited due to complex programming tools. Ziria addresses this problem. It consists of a novel programming language and an optimizing compiler. It is able to synthesize a very efficient SDR code from a high-level PHY description written in Ziria language.
Programming today involves editing code while also running it in our head. To augment this mental simulation, live programming promises for much more fluid feedback between the programmer and a program that is executing while it is being edited.
Crowd-sourcing is increasingly being used for providing answers to online polls and surveys. However, existing systems, while taking care of the mechanics of attracting crowd workers, poll building, and payment, provide little that would help the survey-maker or pollster to obtain statistically significant results devoid of even the obvious selection biases. InterPoll: a platform for programming of crowd-sourced polls. Polls are expressed as embedded LINQ queries, whose results are provided to t
Tabular is a Excel add-in that brings the power of model based machine learning to data enthusiasts. It allows the user to write a simple model that explains their data and perform Bayesian inference. Tabular is built on top of Infer.NET.
Logging is very important for software system development and management. It is crucial to avoid logging too little or too much. To achieve so, developers need to make informed decisions on where to log and what to log in their logging practices during development. However, there exists no work on studying such logging practices in industry or helping developers make informed decisions. In this paper, we systematically study the logging practices of developers.
This project targets at providing code suggestions based on programming context. The suggested code represents usages of an API method.
-- Making it easy for app developers of all levels to test their apps under real-world contexts on the cloud or real devices --
Tempe is a web service for exploratory data analysis.
R2 is a research project within the Programming Languages and Tools group at Microsoft Research India on probabilistic programming. Our goal is to build a user friendly and scalable probabilistic programming system by employing powerful techniques from language design, program analysis and verification.
A domain specific language for writing and analyzing string encoders and decoders.