Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Our research
Content type
+
Downloads (461)
+
Events (467)
 
Groups (151)
+
News (2816)
 
People (717)
 
Projects (1136)
+
Publications (12933)
+
Videos (5999)
Labs
Research areas
Algorithms and theory47205 (360)
Communication and collaboration47188 (238)
Computational linguistics47189 (260)
Computational sciences47190 (245)
Computer systems and networking47191 (810)
Computer vision208594 (934)
Data mining and data management208595 (141)
Economics and computation47192 (124)
Education47193 (89)
Gaming47194 (84)
Graphics and multimedia47195 (250)
Hardware and devices47196 (226)
Health and well-being47197 (104)
Human-computer interaction47198 (982)
Machine learning and intelligence47200 (988)
Mobile computing208596 (81)
Quantum computing208597 (41)
Search, information retrieval, and knowledge management47199 (737)
Security and privacy47202 (358)
Social media208598 (83)
Social sciences47203 (300)
Software development, programming principles, tools, and languages47204 (658)
Speech recognition, synthesis, and dialog systems208599 (160)
Technology for emerging markets208600 (58)
1–25 of 658
Sort
Show 25 | 50 | 100
1234567Next 
Rohit Sinha, Manuel Costa, Akash Lal, Nuno Lopes, Sanjit Seshia, Sriram Rajamani, and Kapil Vaswani

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a...

Publication details
Date: 1 June 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Qingwei LIN, Jian-Guang LOU, Hongyu ZHANG, and Dongmei ZHANG
Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Qingwei LIN, Hongyu ZHANG, Jian-Guang LOU, Yu ZHANG, and Xuewei Chen
Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Miryung Kim, Thomas Zimmermann, Robert DeLine, and Andrew Begel

Creating and running software produces large amounts of raw data about the development process and the customer usage, which can be turned into actionable insight with the help of skilled data scientists. Unfortunately, data scientists with the analytical and software engineering skills to analyze these large data sets have been hard to come by; only recently have software companies started to develop competencies in software-oriented data analytics. To understand this emerging role, we interviewed data...

Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Miryung Kim, Thomas Zimmermann, Robert DeLine, and Andrew Begel

This technical report contains supplemental materials (hierarchical taxonomy of codes, selected quotes) to the paper "The Emerging Role of Data Scientists on Software Development Teams" published at ICSE 2016.

Publication details
Date: 10 February 2016
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2016-4
Ravi Mangal, Xin Zhang, Aditya Kamath, Aditya V. Nori, and Mayur Naik

Many inference problems are naturally formulated using hard and soft constraints over relational domains: the desired solution must satisfy the hard constraints, while optimizing the objectives expressed by the soft constraints. Existing techniques for solving such constraints rely on efficiently grounding a sufficient subset of constraints that is tractable to solve. We present an eager-lazy grounding algorithm that eagerly exploits proofs and lazily refutes counterexamples. We show that our algorithm...

Publication details
Date: 1 February 2016
Type: Inproceeding
Publisher: AAAI - Association for the Advancement of Artificial Intelligence
Pantazis Deligiannis, Matt McCutchen, Paul Thomson, Shuo Chen, Alastair F. Donaldson, John Erickson, Cheng Huang, Akash Lal, Rashmi Mudduluru, Shaz Qadeer, and Wolfram Schulte

Testing distributed systems is challenging due to multiple sources of nondeterminism. Conventional testing techniques, such as unit, integration and stress testing, are ineffective in preventing serious but subtle bugs from reaching production. Formal techniques, such as TLA+, can only verify high-level specifications of systems at the level of logic-based models, and fall short of checking the actual executable code. In this paper, we present a new methodology for testing distributed systems....

Publication details
Date: 1 February 2016
Type: Inproceeding
Luca Cardelli, Attila Csikasz-Nagy, Neil Dalchau, Mirco Tribastone, and Max Tschaikowski

Cells operate in noisy molecular environments via complex regulatory networks. It is possible to understand how molecular counts are related to noise in specific networks, but it is not generally clear how noise relates to network complexity, because different levels of complexity also imply different overall number of molecules. For a fixed function, does increased network complexity reduce noise, beyond the mere increase of overall molecular counts? If so, complexity could provide an advantage...

Publication details
Date: 31 January 2016
Type: Article
Publisher: Nature Publishing Group
Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik
Publication details
Date: 1 January 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman

We present the open-source tool T2, the first public release
from the TERMINATOR project. T2 has been extended over the past
decade to support automatic temporal-logic proving techniques and to
handle a general class of user-provided liveness and safety properties.
Input can be provided in a native format and in C, via the support of
the LLVM compiler framework. We briefly discuss T2’s architecture, its
underlying techniques, and conclude with an experimental illustration...

Publication details
Date: 1 January 2016
Type: Inproceeding
Publisher: Springer
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, and Selva Samuel

We consider the problem of inferring the implicit distribution specified by a probabilistic program.
A popular inference technique for probabilistic programs called Markov Chain Monte Carlo or
MCMC sampling involves running the program repeatedly and generating sample values by
perturbing values produced in “previous runs”. This simulates a Markov chain whose stationary
distribution is the distribution specified by the probabilistic program.
However, it is non-trivial to...

Publication details
Date: 1 December 2015
Type: Inproceeding
Publisher: Leibniz International Proceedings in Informatics
Diego Garbevetsky, Edgardo Zoppi, Thomas Ball, and Benjamin Livshits

In this paper we present the design and implementation of an elastic static analysis framework that is designed to scale with the size of the input. Our approach is based on the actor programming model and is deployed in the cloud. This provides a degree of elasticity for CPU, memory and storage resources.

To demonstrate the potential of our technique, we show how a typical call graph analysis can be implemented. We experimentally validate the analysis using a combination of both synthetic and...

Publication details
Date: 20 November 2015
Type: Technical report
Number: MSR-TR-2015-88
Fei LV, hongyu zhang, Jian-Guang LOU, Shaowei WANG, Dongmei ZHANG, and Jianjun ZHAO
Publication details
Date: 1 November 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Titus Barik, Robert DeLine, Steven Drucker, and Danyel Fisher

Large software organizations are transitioning to event data platforms as they culturally shift to better support data-driven decision making. This paper offers a case study at Microsoft during such a transition. Through qualitative interviews of 28 participants, and a quantitative survey of
1,823 respondents, we catalog a diverse set of activities that leverage event data sources, identify challenges in conducting these activities, and describe tensions that emerge in data-driven cultures as event...

Publication details
Date: 26 October 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-79
Loris D'Antoni, Margus Veanes, Benjamin Livshits, and David Molnar

Tree automata and transducers are used in a wide range of applications in software engineering. While these formalisms are of immense practical use, they can only model finite alphabets. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting infinite alphabets makes these models more general and succinct than their classic counterparts. Despite this, we show how the main operations, such as composition and language...

Publication details
Date: 1 October 2015
Type: Article
Publisher: ACM – Association for Computing Machinery
Number: 1
Pavneet Singh Kochhar, Nachiappan Nagappan, Thomas Zimmermann, and Christian Bird

This document contains the questions in the surveys and interviews used in our study of transitions to open source software at Microsoft.

Publication details
Date: 1 October 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-82
Meredith Ringel Morris, Andrew Begel, and Ben Wiedermann

Technology workers are often stereotyped as being socially awkward or having difficulty communicating, often with humorous intent; however, for many technology workers with atypical cognitive profiles, such issues are no laughing matter. In this paper, we explore the hidden lives of neurodiverse technology workers, e.g., those with autism spectrum disorder (ASD), attention deficit hyperactivity disorder (ADHD), and/or other learning disabilities, such as dyslexia. We present findings from interviews...

Publication details
Date: 1 October 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Awards: Best Paper Award
Veselin Raychev, Madanlal Musuvathi, and Todd Mytkowicz

User-defined aggregations (UDAs) are integral to large-scale data-processing systems, such as MapReduce and Hadoop, because they let programmers express application-specific aggregation logic. System-supported associative aggregations, such as counting or finding the maximum, are data-parallel and thus these systems optimize their execution, leading in many cases to orders-of-magnitude performance improvements. These optimizations, however, are not possible on arbitrary UDAs.

This paper presents...

Publication details
Date: 1 October 2015
Type: Inproceeding
Publisher: USENIX – Advanced Computing Systems Association
Scott Carr and Neil Pittman

Software engineering tools for Hardware Design Languages (HDL) lag behind traditional software development tools by decades. However as heterogeneous computing becomes more pervasive, productive programming in HDLs will become vital. To this end, we have developed gNOSIS a static analysis platform for Verilog HDL. In this project we have extended gNOSIS to support System Verilog. A good analogy is C is to C++ as Verilog is to System Verilog, that is System Verilog is a superset of Verilog with more...

Publication details
Date: 1 September 2015
Type: Technical report
Number: MSR-TR-2015-68
Ravi Mangal, Xin Zhang, Aditya V. Nori, and Mayur Naik

Very large MaxSAT instances, comprising 1020 clauses and beyond, commonly arise in a variety of domains. We present VOLT, a framework for solving such instances, using an iterative, lazy grounding approach. In each iteration, VOLT grounds a subset of clauses in the MaxSAT problem, and solves it using an off-the-shelf MaxSAT solver. VOLT provides a common ground to compare and contrast different lazy grounding approaches for solving large MaxSAT instances. We cast four diverse approaches from the...

Publication details
Date: 1 September 2015
Type: Inproceeding
Publisher: Springer
Shuo Chen

This article provides my recollection about how Prof. José Meseguer enlightened me to study security problems from the logic perspective. His lectures and advices are having a long term influence on my research career.

Publication details
Date: 1 September 2015
Type: Inproceeding
Publisher: Springer
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, and Albert Rubio

We present an automated compositional program
verification technique for safety properties based on conditional
inductive invariants. For a given program part (e.g., a single
loop) and a postcondition ϕ, we show how to, using a Max-SMT
solver, an inductive invariant together with a precondition can be
synthesized so that the precondition ensures the validity of the
invariant and that the invariant implies ϕ. From this, we build
a bottom-up program verification...

Publication details
Date: 1 September 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Yoli Shavit, Boyan Yordanov, Sara-Jane Dunn, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler

A fundamental question in biology is how cells change into specific cell types with unique roles throughout development. This process can be viewed as a program prescribing the system dynamics, governed by a network of genetic interactions. Recent experimental evidence suggests that these networks are not fixed but rather change their topology as cells develop. Currently, there are limited tools for the construction and analysis of such self-modifying biological programs. We introduce Switching Gene...

Publication details
Date: 1 September 2015
Type: Inproceeding
Publisher: Springer
Brittany Johnson, Thomas Zimmermann, and Christian Bird

This reports contains supplemental information: (1) the text of the recruitment survey, (2) the guide for the semi-structured interviews, and (3) the text of the follow-up survey.

Publication details
Date: 28 August 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-66
He Zhu, Aditya V. Nori, and Suresh Jagannathan

We propose the integration of a random test generation system(capable of discovering program bugs) and a refinement type system (capable of expressing and verifying program invariants), for higher-order functional programs, using a novel lightweight learning algorithm as an effective intermediary between the two. Our approach is based on the well-understood intuition that useful, but difficult to infer, program properties can often be observed from concrete program states generated by tests; these...

Publication details
Date: 1 August 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
1–25 of 658
Sort
Show 25 | 50 | 100
1234567Next 
> Our research