Research: Current Projects

PRIME: Programming with Millions of Examples

Programmers make extensive use of frameworks and libraries. To perform standard tasks, such as parsing an XML file or communicating with a database, programmers use standard frameworks rather than writing code from scratch. Unfortunately, a typical framework API can involve hundreds of classes with dozens of methods each, and often requires specific sequences of operations that have to be invoked on specific objects in order to perform a single task. Even experienced programmers might spend hours trying to understand how to use a seemingly simple API. The goal of PRIME is to develop techniques for programming with millions of examples by learning from available public code. PRIME combines static analysis and machine learning techniques to effectively answer semantic code-search queries, code prediction, code completion, and similarity queries. (OOPSLA'12) (SAS'13) (PLDI'14a) (PLDI'14b) (OOPSLA'14) (POPL'16) (PLDI'16) (ICSE'16) (ONWARD'16a)(ONWARD'16b) (PLDI'17) (talk video) (ASPLOS'18a) (ASPLOS'18b) (PLDI'18) (ACL'18) (ICML'18) (POPL'19) (ICLR'19) (PRIME code) (TRACY code) (codota)

Research: Past Projects

Fender: Preserving Correctness under Weak Memory Models

Modern architectures implement relaxed memory models in which memory operations may be reordered and executed nonatomically. Special instructions called memory fences are provided to the programmer, allowing control of this behavior. To ensure correctness of many algorithms, in particular of non-blocking ones, a programmer is often required to explicitly insert memory fences into her program. However, she must use as few fences as possible, or the benefits of running on a relaxed architecture will be lost. Placing memory fences is challenging and extremely error prone, as it requires subtle reasoning about the underlying memory model. The goal of this project is to automatically infer memory fences in concurrent programs, assisting the programmer with this complex task.
(FMCAD'10) (PLDI'11) (PLDI'12) (SA-News'12) (SAS'13) (SAS'14) (DFence Code)

Saint: Synthesis using Abstract Interpretation

Can we generate synchronization code for a program based on a high-level specification of its desired behavior? In this project, we turn the one dimensional problem of verification under abstraction, in which only the abstraction can be modified (typically via abstraction refinement), into a two-dimensional problem, in which both the program and the abstraction can be modified until the abstraction is precise enough to verify the program. We are interested in modifications of a concurrent program that restrict its possible interleavings.
(TACAS'09) (EC2 '09) (SPIN '09) (POPL'10)

Dojo: Ensuring Determinism of Concurrent Systems

One of the main difficulties in parallel programming is the need to reason about possible interleavings of operations in a program. The vast number of interleavings makes this task difficult even for small programs, and impossible for any sizeable software. To simplify reasoning about parallel programs, it is desirable to reduce the number of interleavings that a programmer has to consider. One way to achieve that is to require parallel programs to be deterministic. The goal of this project is to investigate static and dynamic program analysis techniques for checking and enforcing determinism in concurrent systems.
(SAS'10) (RV'10 ) (PLDI'12)

QVM: The Quality Virtual Machine

The Quality Virtual Machine (QVM) is a system that uses the technology and infrastructure available in a virtual machine to improve software quality. QVM provides a framework for easily building dynamic analyses into the VM, continuing the general trend of using additional hardware resources at runtime to help find and/or eliminate bugs.
(OOPSLA'08) (PLDI'09) (ISMM'10) (OOPSLA'11)

Paraglide: Search-Based Synthesis of Concurrent Programs

Current practices for developing concurrent systems are rather limited. Manual constructions using low-level concurrency constructs (e.g. CAS) is the realm of experts, is extremely error-prone and leads to significant non-repeatable effort in both the construction and the verification process. Generic higher-level constructs (e.g., transactional memory) are also limited, and are not clearly easier to use. Analytic techniques (e.g., race detection) only address a fraction of the problems, and can only be applied after the code is written at which point it may be broken beyond repair. The Paraglide project provides construction mechanisms and practical tools that assist the designer in building correct and efficient concurrent systems.
(PLDI'06) (PLDI'07) (PLDI'08) (EC2 '08)

SAFE: Scalable Verification for Heap-Manipulating Programs

The goal of SAFE is to provide a scalable and flexible error-detection tool, based on typestate checking with varying degrees of cost and precision, mostly depending on the way in which aliasing is handled. SAFE can be used for detecting violations of simple correctness properties, and for checking more sophisticated performance properties such as inefficient use of resources.
(ISSTA'06 ) (ISSTA'07 ) (POPL'08) (ISMM'08) (ISSTA'08) (TSE'08) (TOSEM'08) (Mining'11) (Exp'11)

3VMC/TVLA: Shape Analysis for Concurrent Programs

3VMC is a tool for analysis and verification of concurrent systems. 3VMC is geared towards verification of concurrent software, it supports dynamic allocation of objects and threads and does not put an a priori bound on the number of allocated objects and threads.
(POPL'01) (SOFTMC'03) (ESOP'03) (PLDI'04) (IGPL'08) (TOPLAS'10)

Research: Software

• code2seq: Generating Sequences from Structured Representations of Code
• code2vec: Learning Distributed Representations of Code
• Esh: Statistical Similarity of Binaries
• TRACY: tracelet-based search and similarity
• PRIME: programming with millions of examples
• Fender: fence inference and verification under relaxed memory models
• SAFE: typestate checking in presence of aliasing
• 3VMC/TVLA: 3-valued based shape analysis for concurrent programs