Verification and Synthesis of Concurrent Programs
Dr. Eran Yahav (IBM T.J. Watson Research Center, USA)

Practical and efficient concurrent systems are notoriously hard to design, implement, and verify. Current practices for developing concurrent systems are rather limited. Directly using low-level concurrency constructs is the realm of experts, and is extremely error-prone. Generic higher-level constructs (e.g., transactional memory) are currently 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 and is potentially broken in a fundamental manner. In this talk, I will survey recent work of our group on machine-assisted construction of concurrent algorithms.

printable slides





Click in the lower-right corner of the player to go to full screen.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet