CS Colloquium
Tuesday, January 12, 2010
10:30 a.m., AKW 200

Host: Zhong Shao

Sign up to meet with Speaker

Speaker: Dr. Martin Vechev, IBM T.J. Watson Research Center
Title: Abstraction-Guided Synthesis of Synchronization

Abstract: We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually.

Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible.

Combined with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only the abstraction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be verified using the given abstraction.

We implemented a prototype of our approach using numerical abstractions and applied it to verify several interesting programs.

This is joint work with: Eran Yahav and Greta Yorsh.

Bio: Dr. Martin Vechev is a researcher at the IBM Watson Center in New York. He obtained his PhD in 2007 from Cambridge University. His interests are in concurrency, synthesis and verification.