Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Our research
Content type
+
Downloads (448)
+
Events (422)
 
Groups (145)
+
News (2657)
 
People (737)
 
Projects (1069)
+
Publications (12193)
+
Videos (5463)
Labs
Research areas
Algorithms and theory47205 (294)
Communication and collaboration47188 (196)
Computational linguistics47189 (194)
Computational sciences47190 (199)
Computer systems and networking47191 (707)
Computer vision208594 (885)
Data mining and data management208595 (82)
Economics and computation47192 (98)
Education47193 (79)
Gaming47194 (71)
Graphics and multimedia47195 (216)
Hardware and devices47196 (201)
Health and well-being47197 (82)
Human-computer interaction47198 (810)
Machine learning and intelligence47200 (802)
Mobile computing208596 (38)
Quantum computing208597 (20)
Search, information retrieval, and knowledge management47199 (639)
Security and privacy47202 (280)
Social media208598 (29)
Social sciences47203 (248)
Software development, programming principles, tools, and languages47204 (572)
Speech recognition, synthesis, and dialog systems208599 (98)
Technology for emerging markets208600 (28)
1–25 of 572
Sort
Show 25 | 50 | 100
1234567Next 
Emerson Murphy-Hill, Thomas Zimmermann, Christian Bird, and Nachiappan Nagappan

When software engineers fix bugs, they may have several options as to how to fix those bugs. Which fix they choose has many implications, both for practitioners and researchers: What is the risk of introducing other bugs during the fix? Is the bug fix in the same code that caused the bug? Is the change fixing the cause or just covering a symptom? In this paper, we investigate alternative fixes to bugs and present an empirical study of how engineers make design choices about how to fix bugs. We start...

Publication details
Date: 1 December 2015
Type: Article
Publisher: IEEE – Institute of Electrical and Electronics Engineers
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
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
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
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
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
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
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
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
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
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
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
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
Robert A Cochran, Loris D’Antoni, Benjamin Livshits, David Molnar, and Margus Veanes

In this paper, we investigate an approach to program synthesis that is based on crowd-sourcing. With the help of crowd-sourcing, we aim to capture the “wisdom of the crowds” to find good if not perfect solutions to inherently tricky programming tasks, which elude even expert developers and lack an easy-to-formalize specification.

We propose an approach we call program boosting, which involves crowd-sourcing imperfect solutions to a difficult programming problem from developers and then...

Publication details
Date: 1 January 2015
Type: Proceedings
Publisher: ACM – Association for Computing Machinery
Venkatesh Vinayakarao, Rahul Purandare, and Aditya V. Nori

Software developers rarely write code from scratch. With the existence of Wikipedia, discussion forums, books and blogs, it is hard to imagine a software developer not looking up these sites for sample code while building any non-trivial software system. While researchers have proposed approaches to retrieve relevant posts and code snippets, the need for finding variant implementations of functionally similar code snippets has been ignored. In this work, we propose an approach to automatically create a...

Publication details
Date: 1 January 2015
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
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
Aws Albargouthi, Josh Berdine, Byron Cook, and Zachary Kincaid

We propose SplInter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic–based analysis for heap reasoning with (2) an interpolation-based technique for refining heap-shape invariants with data invariants. SplInter is property directed, precise, and produces counterexample traces when a property does not hold. Using the novel notion of spatial interpolants modulo theories, SplInter can infer complex...

Publication details
Date: 1 January 2015
Type: Technical report
Number: MSR-TR-2015-4
He Zhu, Aditya V. Nori, and Suresh Jagannathan

We present a type-based program analysis capable of inferring expressive invariants over array programs. Our system combines dependent types with two additional key elements. First, we associate dependent types with effects and precisely track effectful array updates, yielding a sound flow-sensitive dependent type system that can capture invariants associated with side-effecting array programs. Second, without imposing an annotation burden for quantified invariants on array indices, we automatically...

Publication details
Date: 1 January 2015
Type: Inproceeding
Publisher: Springer
Andreas Frohlich, Armin Biere, Christoph M. Wintersteiger, and Youssef Hamadi

Satisfiability Modulo Theories (SMT) is essential for many practical applications, e.g., in hard- and software verification, and increasingly also in other scientific areas like computational biology. A large number of applications in these areas benefit from bit-precise reasoning over finite-domain variables. Current approaches in this area translate a formula over bit-vectors to an equisatisfiable propositional formula, which is then given to a SAT solver. In this paper, we present a novel stochastic...

Publication details
Date: 1 January 2015
Type: Inproceeding
Publisher: AAAI - Association for the Advancement of Artificial Intelligence
Menghui Lim, Jian-Guang LOU, Hongyu Zhang, Qiang FU, Andrew Teoh, Qingwei LIN, Rui Ding, and Dongmei Zhang

For a large-scale software system, especially an online service system, when a performance issue occurs, it is desirable to check whether this issue has occurred before. If there are past similar issues, a known remedy could be applied. Otherwise, a new troubleshooting process may have to be initiated. The symptom of a performance issue can be characterized by a set of metrics. Due to the sophisticated nature of software systems, manual diagnosis of performance issues based on metric data is typically...

Publication details
Date: 14 December 2014
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Tom Crick, Benjamin A. Hall, Samin Ishtiaq, and Kenji Takeda

The reproduction and replication of reported scientific results is a hot topic within the academic community. The retraction of numerous studies from a wide range of disciplines, from climate science to bioscience, has drawn the focus of many commentators, but there exists a wider socio-cultural problem that pervades the scientific community. Sharing data and models often requires extra effort, and this is currently seen as a significant overhead that may not be worth the time investment....

Publication details
Date: 1 December 2014
Type: Inproceeding
Zhenyu Guo, Cheng Chen, Haoxiang Lin, Sean McDirmid, Fan Yang, Xueying Guo, Mao Yang, and Lidong Zhou

Our cloud services are losing too many battles to faults like software bugs, resource interference, and hardware failures. Many tools can help us win these battles: model checkers to verify, fault injection to find bugs, replay to debug, and many more. Unfortunately, tools are currently afterthoughts in cloud service designs that must either be tediously tangled into service implementations or integrated transparently in ways that fail to effectively capture the service’s problematic non-deterministic...

Publication details
Date: 26 November 2014
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2014-150
1–25 of 572
Sort
Show 25 | 50 | 100
1234567Next 
> Our research