Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Our research
Content type
+
Downloads (455)
+
Events (485)
 
Groups (150)
+
News (2840)
 
People (723)
 
Projects (1159)
+
Publications (12963)
+
Videos (6110)
Labs
Research areas
Algorithms and theory47205 (375)
Communication and collaboration47188 (247)
Computational linguistics47189 (267)
Computational sciences47190 (245)
Computer systems and networking47191 (843)
Computer vision208594 (948)
Data mining and data management208595 (164)
Economics and computation47192 (129)
Education47193 (91)
Gaming47194 (85)
Graphics and multimedia47195 (255)
Hardware and devices47196 (235)
Health and well-being47197 (115)
Human-computer interaction47198 (1010)
Machine learning and intelligence47200 (1022)
Mobile computing208596 (88)
Quantum computing208597 (41)
Search, information retrieval, and knowledge management47199 (750)
Security and privacy47202 (366)
Social media208598 (91)
Social sciences47203 (315)
Software development, programming principles, tools, and languages47204 (680)
Speech recognition, synthesis, and dialog systems208599 (178)
Technology for emerging markets208600 (64)
1–25 of 680
Sort
Show 25 | 50 | 100
1234567Next 
Rishabh Singh

The recent Programming By Example (PBE) techniques such as FlashFill have shown great promise for enabling end-users to perform data transformation tasks using input-output examples. Since examples are inherently an under-specification, there are typically a large number of hypotheses conforming to the examples, and the PBE techniques suffer from scalability issues for finding the intended program amongst the large space.

We present a semi-supervised learning technique to significantly reduce...

Publication details
Date: 1 September 2016
Type: Inproceeding
Publisher: VLDB – Very Large Data Bases
Aleksandar Zeljic, Christoph M. Wintersteiger, and Philipp Rummer

The Model-Constructing Satisfiability Calculus (mcSAT) is a recently proposed generalisation of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry out con ict-driven learning only on the propositional level, mcSAT calculi can also synthesise new theory literals during learning, resulting in a simple yet very exible framework for designing efficient decision procedures. We present an mcSAT calculus for the theory of bounded-length...

Publication details
Date: 1 July 2016
Type: Inproceeding
Publisher: Springer
Loris D'Antoni, Roopsha Samanta, and Rishabh Singh

The goal of automatic program repair is to identify a set of syntactic changes
that can turn a program that is incorrect with respect to a given specification into a correct one.
Existing program repair techniques typically
aim to find any program that meets the given specification.
Such ``best-effort'' strategies can end up generating a program that is quite different
from the original one.
Novel techniques have been proposed to compute syntactically minimal program...

Publication details
Date: 1 July 2016
Type: Inproceeding
Loris D'Antoni and Margus Veanes

Symbolic tree automata allow transitions to carry predicates over rich alphabet theories, such as linear arithmetic, and therefore extend finite tree automata to operate over infinite alphabets, such as the set of rational numbers. Existing tree automata algorithms rely on the alphabet being finite, and generalizing them to the sym bolic setting is not a trivial task.

In this paper we study the problem of minimizing symbolic tree automata. First, we formally define and prove the basic prope rties...

Publication details
Date: 1 July 2016
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl

We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs. To this end, we construct symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs. We...

Publication details
Date: 1 June 2016
Type: Inproceeding
Publisher: Springer
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
Parmit K. Chilana, Rishabh Singh, and Philip J. Guo

Recent research suggests that some students learn to program with the goal of becoming conversational programmers: they want to develop programming literacy skills not to write code in the future but mainly to develop conversational skills and communicate better with developers and to improve their marketability. To investigate the existence of such a population of conversational programmers in practice, we surveyed professionals at a large multinational technology company who were not in...

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
Thomas Ball, Jonathan Protzenko, Judith Bishop, Michał Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, and Clare Riley

The chance to influence the lives of a million children does not come often. Through a partnership between the BBC and several technology companies, a small instructional computing device called the BBC micro:bit will be given to a million children in the UK in 2016. Moreover, using the micro:bit will be part of the CS curriculum. We describe how Microsoft's Touch Develop programming platform works with the BBC micro:bit. We describe the design and architecture of the micro:bit and the software...

Publication details
Date: 1 May 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
Prem Devanbu, Thomas Zimmermann, and Christian Bird

Empirical software engineering has produced a steady stream of evidence-based results concerning the factors that affect important outcomes such as cost, quality, and interval. However, programmers often also have strongly-held a priori opinions about these issues. These opinions are important, since developers are highlytrained professionals whose beliefs would doubtless affect their practice. As in evidence-based medicine, disseminating empirical findings to developers is a key step in...

Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Weidong Cui, Marcus Peinado, Sang Kil Cha, Yanick Fratantonio, and Vasileios P. Kemerlis

Many software providers operate crash reporting services to automatically collect crashes from millions of customers and file bug reports. Precisely triaging crashes is necessary and important for software providers because the millions of crashes that may be reported every day are critical in identifying high impact bugs. However, the triaging accuracy of existing systems is limited, as they rely only on the syntactic information of the stack trace at the moment of a crash without analyzing program...

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
Michael Washburn Jr, Pavithra Sathiyanarayanan, Meiyappan Nagappan, Thomas Zimmermann, and Christian Bird

In game development, software teams often conduct postmortems to reflect on what went well and what went wrong in a project. The postmortems are shared publicly on gaming sites or at developer conferences. In this paper, we present an analysis of 155 postmortems published on the gaming site Gamasutra.com. We identify characteristics of game development, link the characteristics to positive and negative experiences in the postmortems and distill a set of best practices and pitfalls for game...

Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Edward K. Smith, Christian Bird, and Thomas Zimmermann

In this paper we present the results from a survey about the beliefs, practices, and personalities of software engineers in a large software company. The survey received 797 responses. We report statistics about beliefs of software engineers, their work practices, as well as differences in those with respect to personality traits. For example, we observed no personality differences between developers and testers; managers were conscientious and more extraverted. We observed several differences for...

Publication details
Date: 1 May 2016
Type: Inproceeding
Publisher: ACM – Association for Computing Machinery
Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl

We present a modular approach to automatic complexity analysis of integer programs. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer bounds on the absolute values of program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. The bounds computed by our method are polynomial or exponential expressions that depend on the absolute values of input parameters.
We show how to...

Publication details
Date: 1 April 2016
Type: Article
Publisher: ACM – Association for Computing Machinery
Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow, and He Zhu

We present a data-driven verification framework to automatically prove memory safety and functional correctness of heap programs. For this, we introduce a novel statistical machine learning technique that maps observed program states to (possibly disjunctive) separation logic formulas describing the invariant shape of data structures at relevant program locations. We then attempt to verify these predictions using a theorem prover, where counterexamples to a predicted invariant are used as additional...

Publication details
Date: 1 April 2016
Type: Technical report
Number: MSR-TR-2016-17
Zvonimir Pavlinovic, Akash Lal, and Rahul Sharma

Finding invariants is an important step in automated program analysis. Discovery of precise invariants, however, can be very difficult in practice. The problem can be simplified if one has access to a candidate set of predicates (or annotations) and the search for invariants is limited over the space defined by these annotations. We present an approach that infers program annotations automatically by leveraging the history of verifying related programs. Our algorithm extracts high-quality...

Publication details
Date: 1 April 2016
Type: Technical report
Publisher: Microsoft Research
Number: MSR-TR-2016-15
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: 23 March 2016
Type: Technical report
Number: MSR-TR-2016-13
Yun-Nung Chen, Dilek Hakkani-Tur, and Xiaodong He

The recent surge of intelligent personal assistants motivates spoken language understanding of dialogue systems. However, the domain constraint along with the inflexible intent schema remains a big issue. This paper focuses on the task of intent expansion, which helps remove the domain limit and make an intent schema flexible. A convolutional deep structured semantic model (CDSSM) is applied to jointly learn the representations for human intents and associated utterances. Then it can flexibly generate...

Publication details
Date: 1 March 2016
Type: Inproceeding
Publisher: IEEE – Institute of Electrical and Electronics Engineers
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
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
1–25 of 680
Sort
Show 25 | 50 | 100
1234567Next 
> Our research