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
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.
There is some evidence that a gap exists between the neural network research and software development communities. Source code examples available to software developers are often incomplete, misleading, or just plain incorrect. The goal of this project is to bridge that gap by providing a series of high quality demo programs.
Pex4Fun is a browser-based teaching and learning environment targeting teachers and students for introductory to advanced programming or software engineering courses. At the core of the platform is an automated grading engine based on symbolic execution. In Pex4Fun, teachers can create virtual classrooms, customize existing courses, and publish new learning material including learning games.
The Q program verifier is a collection of front-ends that compile different source languages to an intermediate representation (IR), and back-ends that perform verification on the IR. Together, Q is a verification platform that hosts multiple tools and technologies for analyzing properties of programs.
Automatic program verification tool for proving temporal properties of programs
Code Digger is a Microsoft® Visual Studio® 2012 and 2013 extension that analyzes possible execution paths through your .NET code. The result is a table where each row shows a unique behavior of your code. The table helps you understand the behavior of the code, and it may also uncover hidden bugs.
Intelligent Tutoring Systems (ITS) can significantly enhance the educational experience, both in the classroom and online. A key aspect of ITS is the ability to automatically generate problems of a certain difficulty level and that exercise use of certain concepts. This can help avoid copyright or plagiarism issues and help generate personalized workflows. This project develops technologies for problem generation in various subject domains including math, logic, and even language learning.
Programming models such as HIVE and DryadLINQ provide programmers with simple declarative abstractions for writing data intensive computations that can run on a large cluster of machines. However, this level of abstraction comes at a cost – the inability to understand, predict and debug performance. This project aims at building performance models for predicting the performance of the query while identifying bottleneck resources and computations.
The goal of the Dandelion project is to provide simple programming abstractions and runtime supports for programming heterogeneous systems. Dandelion supports a uniform sequential programming model across a diverse array of execution contexts, including CPU, GPU, FPGA, and the cloud.