Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Our research
Content type
+
Downloads (449)
+
Events (427)
 
Groups (147)
+
News (2665)
 
People (738)
 
Projects (1079)
+
Publications (12262)
+
Videos (5512)
Labs
Research areas
Algorithms and theory47205 (307)
Communication and collaboration47188 (202)
Computational linguistics47189 (205)
Computational sciences47190 (200)
Computer systems and networking47191 (721)
Computer vision208594 (892)
Data mining and data management208595 (88)
Economics and computation47192 (98)
Education47193 (79)
Gaming47194 (73)
Graphics and multimedia47195 (222)
Hardware and devices47196 (201)
Health and well-being47197 (84)
Human-computer interaction47198 (821)
Machine learning and intelligence47200 (826)
Mobile computing208596 (44)
Quantum computing208597 (22)
Search, information retrieval, and knowledge management47199 (647)
Security and privacy47202 (285)
Social media208598 (35)
Social sciences47203 (248)
Software development, programming principles, tools, and languages47204 (586)
Speech recognition, synthesis, and dialog systems208599 (104)
Technology for emerging markets208600 (28)
1–25 of 586
Sort
Show 25 | 50 | 100
1234567Next 
Abram Hindle, Christian Bird, Thomas Zimmermann, and Nachiappan Nagappan

Large organizations like Microsoft tend to rely on formal requirements documentation in order to specify and design the software products that they develop. These documents are meant to be tightly coupled with the actual implementation of the features they describe. In this paper we evaluate the value of high-level topic-based requirements traceability and issue report traceability in the version control system, using Latent Dirichlet Allocation (LDA). We evaluate LDA topics on practitioners...

Publication details
Date: 1 December 2015
Type: Article
Publisher: Springer
Akash Lal and Shaz Qadeer

A hierarchical program is one with multiple procedures but no loops or recursion. This paper studies the problem of deciding reachability queries in hierarchical programs. This problem is fundamental to verification and most directly applicable to doing bounded reachability in programs, i.e., reachability under a bound on the number of loop iterations and recursive calls.

The usual method of deciding reachability in hierarchical programs is to first
inline all procedures and then do...

Publication details
Date: 1 June 2015
Type: Inproceeding
Publisher: ACM
Pantazis Deligiannis, Jeroen Ketema, Paul Thomson, Alastair Donaldson, and Akash Lal

Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against interleaving-dependent bugs such as data races and other assertion violations. Previous work has only addressed these challenges individually, either by designing a new declarative language, or a new data race detection tool, or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static analysis...

Publication details
Date: 1 June 2015
Type: Inproceeding
Publisher: ACM
Christopher Theisen, Kim Herzig, Patrick Morrison, Brendan Murphy, and Laurie Williams

Security testing and reviewing efforts are a necessity for software projects, but are time-consuming and expensive to apply. Identifying vulnerable code supports decision-making during all phases of software development. An approach for identifying vulnerable code is to identify its attack surface, the sum of all paths for untrusted data into and out of a system. Identifying the code that lies on the attack surface requires expertise and significant manual effort. This paper proposes an...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Edward K. Smith, Christian Bird, and Thomas Zimmermann

Developers sometimes take the initiative to build tools to solve problems they face. What motivates developers to build these tools? What is the value for a company? Are the tools built useful for anyone besides their creator? We conducted a qualitative study of tool building, adoption, and impact within Microsoft. This paper presents our findings on the extrinsic and intrinsic factors linked to toolbuilding, the value of building tools, and the factors associated with tool spread. We find that the...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Michael Barnett, Christian Bird, Joao Brunet, and Shuvendu Lahiri

Code Reviews, an important and popular mechanism for quality assurance, are often performed on a changeset, a set of modified files that are meant to be committed to a source repository as an atomic action. Understanding a code review is more difficult when the changeset consists of multiple, independent, code differences. We introduce CLUSTERCHANGES, an automatic technique for decomposing changesets and evaluate its effectiveness through both a quantitative analysis and a qualitative...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Kim Herzig, Michaela Greiler, Jacek Czerwonka, and Brendan Murphy

Testing is a key element of software development processes for the management and assessment of product quality. In most development environments, the software engineers are responsible for ensuring the functional correctness of code. However, for large complex software products, there is an additional need to check that changes do not negatively impact other parts of the software and they comply with system constraints such as backward compatibility, performance, security etc. Ensuring these system...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Kim Herzig and Nachiappan Nagappan

Applying code changes to software systems and testing these code changes can be a complex task that involves many different types of software testing strategies, e.g. system and integration tests. However, not all test failures reported during code integration are hinting towards code defects. Testing large systems such as the Microsoft Windows operating system requires complex test infrastructures, which may lead to test failures caused by faulty tests and test infrastructure issues. Such false test...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Eric Chen, Shuo Chen, Shaz Qadeer, and Rui Wang

The prevalence of security flaws in multiparty online services (e.g., single-sign-on, third-party payment, etc.) calls for rigorous engineering supported by formal program verification. However, the adoption of program verification faces several hurdles in the real world: how to formally specify logic properties given that protocol specifications are often informal and vague; how to precisely model the attacker and the runtime platform; how to deal with the unbounded set of all potential...

Publication details
Date: 1 May 2015
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Martín Abadi and Michael Isard

Publication details
Date: 1 April 2015
Type: Inproceeding
Publisher: Springer
Patrick Morrison, Kim Herzig, Brendan Murphy, and Laurie Williams

While Microsoft product teams have adopted defect prediction models, they have not adopted vulnerability prediction models (VPMs). Seeking to understand this discrepancy, we replicated a VPM for two releases of the Windows Operating System, varying model granularity and statistical learners. We reproduced binary-level prediction precision (~0.75) and recall (~0.2). However, binaries often exceed 1 million lines of code, too large to practically inspect, and engineers expressed preference for source file...

Publication details
Date: 1 April 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Martn Abadi and michael isard

We study information ow in a model for data-parallel computing. We show how an extant notion of virtual time can help guarantee information- ow properties. For this purpose, we introduce functions that express dependencies between inputs and outputs at each node in a data ow graph. Each node may operate over a distinct set of virtual times|so, from a security perspective, it may have its own classification scheme. A coherence criterion ensures that those local dependencies yield global properties.

Publication details
Date: 1 April 2015
Type: Inproceeding
Publisher: Springer
Martín Abadi and Michael Isard

We study information ow in a model for data-parallel computing. We show how an extant notion of virtual time can help guarantee information- ow properties. For this purpose, we introduce functions that express dependencies between inputs and outputs at each node in a data ow graph. Each node may operate over a distinct set of virtual times|so, from a security perspective, it may have its own classification scheme. A coherence criterion ensures that those local dependencies yield global properties.

Publication details
Date: 1 April 2015
Type: Inproceeding
Publisher: Springer
Martín Abadi and Michael Isard

Publication details
Date: 1 April 2015
Type: Inproceeding
Publisher: Springer
Ankush Desai, Shaz Qadeer, Sriram Rajamani, and Sanjit Seshia

Liveness specifications on finite-state concurrent programs are checked using algorithms to detect reachable cycles in the state-transition graph of the program. We present new algorithms for cycle detection based on the idea of prioritized search via a delaying explorer. We present thorough evaluation of our algorithms on a variety of reactive asynchronous programs, including device drivers, distributed protocols, and other benchmarks culled from the research literature.

Publication details
Date: 25 March 2015
Type: Technical report
Number: MSR-TR-2015-28
Erdal Mutlu, Serdar Tasiran, and Benjamin Livshits

As JavaScript has become virtually omnipresent as the language for programming large and complex web applications in the last several years, we have seen an increase in interest in finding data races in client-side JavaScript. While JavaScript execution is single-threaded, there is still enough potential for data races, created largely by the nondeterminism of the scheduler. Recently, several academic efforts have explored both static and runtime analysis approaches in an effort to find data races....

Publication details
Date: 17 March 2015
Type: Technical report
Number: MSR-TR-2015-24
Gordon Stewart, Mahanth Gowda, Geoffrey Mainland, Bozidar Radunovic, Dimitrios Vytiniotis, and Cristina Luengo Agulló

Software-defined radio (SDR) brings the flexibility of software to wireless protocol design, promising an ideal platform for innovation and rapid protocol deployment. However, implementing modern wireless protocols on existing SDR platforms often requires careful hand-tuning of low-level code, which can undermine the advantages of software.

Ziria is a new domain-specific language (DSL) that offers programming abstractions suitable for wireless physical (PHY) layer tasks while emphasizing the...

Publication details
Date: 1 March 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, and Zvonimir Rakamaric

SMACK and Corral are two components of a modular toolchain for verifying C programs. Together they exploit state-of-the-art compiler technologies and theorem provers to simplify and dispatch verification conditions.

Publication details
Date: 1 March 2015
Type: Inproceeding
Publisher: Springer
Ankush Desai, Shaz Qadeer, and Sanjit Seshia

We introduce the concept of a delaying explorer with the
goal of performing prioritized exploration of the behaviors
of an asynchronous reactive program. A delaying explorer
stratifies the search space using a custom strategy, and a de-
lay operation that allows deviation from that strategy. We
show that prioritized search with a delaying explorer per-
forms significantly better than existing prioritization tech-
niques. We also demonstrate empirically the need for...

Publication details
Date: 1 March 2015
Type: Technical report
Number: MSR-TR-2015-25
Ben Stock, Ben Livshits, and Ben Zorn

In recent years, the drive-by malware space has undergone significant consolidation. Today, the most common source of drive-by downloads are the so-called exploit kits. Exploit kits signify a drastic consolidation of the process of malware creation and delivery. This paper presents Kizzle, the first prevention technique specifically designed for finding exploit kits.

Our analysis of exploit kits shows that while the actual JavaScript delivered by kits varies greatly, the code observed after it is...

Publication details
Date: 13 February 2015
Type: Technical report
Number: MSR-TR-2015-12
Christian Bird, Trevor Carnahan, and Michaela Greiler

Tool based code review is growing in popularity and has become a standard part of the development process at Microsoft. Adoption of these tools make it possible to mine data from code reviews and provide access to it. In this paper, we present an experience report for CodeFlow Analytics, a system that collects code review data, generates metrics from this data, and provides a number of ways for development teams to access the metrics and data. We discuss the design, design decisions and challenges that...

Publication details
Date: 1 February 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-22
Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran

We present CIVL, a language and verifier for concurrent programs based on automated and modular refinement reasoning. CIVL supports reasoning about a concurrent program at many levels of abstraction. Atomic actions in a high-level description are refined to fine-grain and optimized lower-level implementations. Modular specifications and proof annotations, such as location invariants and procedure pre- and post-conditions, are specified separately, independently at each level in terms of the variables...

Publication details
Date: 1 February 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-8
Maria Christakis and Patrice Godefroid

We present IC-Cut, short for “Interface-Complexity based Cut”, a new compositional search strategy for systematically testing large programs. IC-Cut dynamically detects function interfaces that are simple enough to be cost-effective for summarization. IC-Cut then hierarchically decomposes the program into units defined by such functions and their sub-functions in the call graph. These units are tested independently, their test results are recorded as low-complexity function summaries, and the summaries...

Publication details
Date: 1 February 2015
Type: Technical report
Number: MSR-TR-2015-10
Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich

In the age of cloud-connected mobile devices, users want responsive apps that read and write shared data everywhere, at all times, even if network connections are slow or unavailable. The solution is to replicate data and propagate updates asynchronously. Unfortunately, such mechanisms are notoriously difficult to understand, explain, and implement.

To address these challenges, we present GSP (global sequence protocol), an operational model for replicated shared data. GSP is simple and abstract...

Publication details
Date: 1 January 2015
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2015-11
Thomas BALL and Jakub DANIEL

Dynamic symbolic execution (DSE) is a well-known technique for automatically generating tests to achieve higher levels of coverage in a program. Two keys ideas of DSE are to: (1) seed symbolic execution by executing a program on an initial input; (2) using concrete values from the program execution in place of symbolic expressions whenever symbolic reasoning is hard or not desired. We describe DSE for a simple core language and then present a minimalist implementation of DSE for Python (in Python) that...

Publication details
Date: 1 January 2015
Type: Article
Publisher: IOS Press
1–25 of 586
Sort
Show 25 | 50 | 100
1234567Next 
> Our research