Current Projects

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)

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)

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'10best paper award) (PLDI'12)

Completed Projects

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 best paper award) (ISSTA'07 best paper award Pat Goldberg Best Paper Award) (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)

Software