Previous terms: S10 F08 S08 W08 F07 W07 F06 S06 W06
|Date||Speaker||Title (click for abstract)||Location|
|Thu. Nov. 25, 2010 at 1:00||Martin Vechev||Techniques for Building Correct and Efficient Concurrent Systems||DC 1331|
All are welcome.
Talk announcements are also posted to a public mailing list.
To volunteer to give a talk, contact Ondřej Lhoták. Talks can range from informal to formal, and they can be about any of the following:
The purpose is for us all to see what people are interested in, and motivate discussions.
In this talk, I will survey some of the techniques we have developed for automatically synthesizing correct and efficient synchronization. I will then focus on a new approach that combines classic abstract interpretation and synchronization inference. The essence of this technique lays in its bidirectional nature: to produce a correct concurrent program, at any step, an automatic verifier can now manipulate both: i) the program by introducing synchronization, or ii) the abstraction by refining it or coarsening it.
Finally, I will present a new result which states that it is impossible to build correct concurrent implementations of virtually all known abstract data types such as stacks, sets, queues, hash tables, and others, without using certain very expensive synchronization. This result has implications on hardware architectures, concurrent algorithm design, and synchronization inference.
Martin Vechev is a researcher at the IBM T.J. Watson Center in New York. He obtained his PhD in 2007 from Cambridge University. His interests are in concurrency, analysis, and verification.