590P (Programming Languages Research seminar) and 590N (Software Engineering Research seminar) will meet together this quarter on Tuesdays at 1:30PM in EE 045. We will have 10 research presentations this quarter from the Microsoft Research RISE (Research in Software Engineering) group, which covers a broad array of topics from compilers to human aspects of software engineering.

oct 6  

rob deline  

the social programmer [slides]

oct 13  

tom zimmerman  

cross-project defect prediction [slides]

oct 20  

nicolaj bjorner  

z3: an efficient smt solver [slides]

oct 27  

manuel fahndrich  

language agnostic specification and verification for .net [slides]

nov 3  

patrice godefroid  

software model checking improving security of a billion computers [slides]

nov 10  

ben zorn  

fault tolerant, efficient, and secure runtime systems [slides]

nov 17  

francesco logozzo  

clousot: a static contract checker based on abstract interpretation [slides]

nov 24  

ben livshits  

dec 1  

trishul chilimbi  

dec 8  

ethan jackson  

rob deline: the social programmer [slides]

Despite stereotypes to the contrary, software development is a very social activity. Developers spend a large fraction of their time in conversation with team mates, seeking information, coordinating activities, and building consensus about design decisions. The downside, though, is that their work is often interrupted or blocked on missing information, which leads to a frustratingly fragmented work day. In this talk, we'll examine this behavior in detail, with an eye toward productivity drains. I'll describe several prototype development tools from Microsoft Research that help developers find the people and information they need and cope with interruptions.

tom zimmerman: cross-project defect prediction [slides]

Defect prediction works well within projects as long as there is a sufficient amount of data available to train any models. However, this is rarely the case for new software projects and for many companies. So far, only few studies have focused on transferring prediction models from one project to another. In this talk, I will report on a large-scale study of cross-project defect prediction models, in which we found that Firefox can predict defects in IE, but not vice versa. To understand why, we identified factors that do influence the success of cross-project predictions.

Optional background reading is: Thomas Zimmermann, Nachiappan Nagappan, Andreas Zeller. Predicting Bugs from History. In Software Evolution (Software Evolution), February 2008, pp. 69-88.

The chapter is freely available at Springer (under Sample pages).

nicolaj bjorner: z3: an efficient smt solver [slides]

The area of software analysis, testing and verification is now undergoing a revolution thanks to the use of automated and scalable support for logical methods. A well-recognized premise is that at the core of software analysis engines is invariably a component using logical formulas for describing states and transformations between system states. One can thus say that symbolic logic is the calculus of computation.

Satisfiability Modulo Theories (SMT) solvers can be used to check the satisfiability of logical formulas over one or more theories. SMT solvers offer a compelling match for software and hardware applications, since several common constructs map directly into supported theories.

This seminar will present the state-of-the-art SMT solver Z3, developed at Microsoft Research, Redmond by Leonardo de Moura and Nikolaj Bjorner.

manuel fahndrich: language agnostic specification and verification for .net [slides]

Specifying application interfaces (APIs) with information that goes beyond method argument and return types is a long-standing quest of programming language researchers and practitioners. The number of type system extensions or specification languages in the literature is a testament to that.

This talk presents a new approach to specification languages using an embedding of contracts as code. We will discuss the numerous advantages of our approach, as well as the technical challenges.

Contracts are targeted at the general developer, not the verification enthusiast. It is thus important that a single form of specification meets three simultaneous goals:

• First and foremost, contracts serve as documentation. They must be as readable as possible.
• Second, contracts should be executable. This motivates writing specifications for testing and immediate perceived benefit, without consideration of static verification.
• Finally, contracts should help in static defect discovery and reduce false positives.

Our specification approach is language-agnostic in that we use idiomatic code written in the developer's source language to express preconditions, postconditions, and object invariants.

patrice godefroid: software model checking improving security of a billion computers [slides]

I will present a form of software model checking that has improved the security of a billion computers (and has saved Microsoft millions of dollars). This form of software model checking is dubbed whitebox fuzz testing, and builds upon recent advances in systematic dynamic test generation (also known as DART) and constraint solving. Starting with a well-formed input, whitebox fuzzing symbolically executes the sequential program under test dynamically, and gathers constraints on inputs from conditional statements encountered along the execution. The collected constraints are negated systematically one-by-one and solved with a constraint solver, yielding new inputs that exercise different execution paths in the program. This process is repeated using novel state-space exploration techniques that attempt to sweep through all (in practice, many) feasible execution paths of the program while checking simultaneously many properties. This approach thus combines program analysis, testing, model checking and automated theorem proving (constraint solving).

Whitebox fuzzing has been implemented in the tool SAGE, which is optimized for long symbolic executions at the x86 binary level. Over the past 18 months, SAGE has been running 24/7 on hundreds of machines and has discovered many new expensive security-critical bugs in large shipped Windows applications, including image processors, media players and file decoders, that are deployed on more than a billion computers worldwide. Notably, SAGE has found roughly 1/3 of all Windows7 file-fuzzing bugs. SAGE is so effective in finding bugs missed by other techniques like static analysis or blackbox random fuzzing that it is now used daily in various Microsoft groups.

This is joint work with Michael Levin (Microsoft CSE) and other contributors.

Extra: I will conclude by briefly discussing two related projects at MSR (namely PEX and YOGI) and future work.

ben zorn: fault tolerant, efficient, and secure runtime systems [slides]

Software bugs have long been a source of security vulnerabilities and low reliability. Traditional runtime solutions, such as bounds checking, attempt to detect memory corruptions before they happen and stop the program from continuing to execute unsafely. This strategy has the disadvantage that the user still experiences an unexpected program failure and loss of service. Even worse, as hardware becomes more unreliable, bounds checking fails to detect and/or prevent data corruption caused by hardware faults.

In this talk, I will discuss the design and implementation of runtime systems designed to tolerate memory corruption faults cause by either software or hardware. I will discuss Exterminator, a runtime system that can automatically tolerate, detect, and correct buffer overruns and dangling pointer errors. I will also present Samurai, a runtime that allows programmers to distinguish "critical data", which the runtime supports with additional guarantees against memory corruptions. I will show that such runtime systems can be both efficient and effective at tolerating errors. Commercial examples of such an approach, including the Fault Tolerant Heap in Windows 7, demonstrate that fault tolerant runtimes are both viable and effective.

Exterminator is joint research with Emery Berger and Gene Novark, and Samurai is joint research with Karthik Pattabiraman.

francesco logozzo: clousot: a static contract checker based on abstract interpretation [slides]

I will give an overview (and some demos ;-) of Clousot the static contract checker included in CodeContracts.

CodeContracts allow to use code to specify contracts in .NET.

Unlike similar tools, Clousot is based on abstract interpretation, and this gives a series of advantages: (i) automatic inference of loop invariants; (ii) predictability (the analysis follows the structure and semantics of the program); and (iii) scalability (the analyzer focuses on properties of interest).

In the talk I will describe the structure of Clousot, some of its design choices (e.g. the analysis of bytecode), and some of the new abstract domains we developed to infer linear inequalities (Subpolyhedra) and properties of arrays.

No deep pre-knowledge of abstract interpretation is required ;-)