Campus Event Calendar
Event Entry
What and Who
Machine-Assisted Concurrent Programming
Martin Vechev
IBM T.J. Watson Research Center in New York
SWS Colloquium
Martin Vechev is a Research Staff Member at the IBM T.J. Watson Research Center in New York.
His research interests are in software analysis, programming languages, verification, and concurrency.
He is interested in developing tools and techniques that improve software quality and programmer productivity.
He is the recipient of a Best Paper Award, IBM Research Outstanding Technical Achievement and
Extraordinary Accomplishment Awards and a John Atanasoff Award, awarded by the president of Bulgaria.
He holds a B.Sc. from Simon Fraser University, Canada, and a Ph.D. from the University of Cambridge, England.
SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 18 April 2011
11:00
90 Minutes
G26
206
Kaiserslautern
Abstract
Virtually all chips today are built with an increasing number of processor cores.
To leverage these hardware trends, all future software will have to be concurrent.
The main challenge in developing reliable concurrent software is that a programmer
is forced to coordinate a fantastic number of possible interactions. Manual coordination
of these interactions (e.g., via locks) has proven to be extremely time consuming,
and brittle, often resulting in programs that are incorrect, do not fully utilize the underlying
computational resources, or both.
In this talk, I will present new techniques that harness the growing power of modern
hardware and the increasing maturity of formal methods to simplify the process of
program construction: in essence, given a concurrent program that violates a desired
property, the techniques will analyze the (possibly infinite-state) program and attempt
to automatically repair it by synthesizing the necessary synchronization.
A tool implementing these techniques has been successfully applied to a variety
of challenging problems: from discovering tricky synchronization under weak memory models,
to enforcing general atomicity properties, to obtaining new concurrent data structures
and memory management algorithms.
To leverage these hardware trends, all future software will have to be concurrent.
The main challenge in developing reliable concurrent software is that a programmer
is forced to coordinate a fantastic number of possible interactions. Manual coordination
of these interactions (e.g., via locks) has proven to be extremely time consuming,
and brittle, often resulting in programs that are incorrect, do not fully utilize the underlying
computational resources, or both.
In this talk, I will present new techniques that harness the growing power of modern
hardware and the increasing maturity of formal methods to simplify the process of
program construction: in essence, given a concurrent program that violates a desired
property, the techniques will analyze the (possibly infinite-state) program and attempt
to automatically repair it by synthesizing the necessary synchronization.
A tool implementing these techniques has been successfully applied to a variety
of challenging problems: from discovering tricky synchronization under weak memory models,
to enforcing general atomicity properties, to obtaining new concurrent data structures
and memory management algorithms.
Contact
Maria-Louise Maggio
9604
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
5th floor, Wartburg
passcode not visible
logged in users only
Maria-Louise Maggio, 04/13/2011 13:03 -- Created document.