ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Corneliu Popeea , Max Plank Institute for Software Systems
When:2009-12-23 15:00
Place:Room 309-1, Bldg 302, SNU


Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment assumptions, to enable scalable reasoning. Once identified, these assumptions can be used for reasoning with one program thread at a time, which is possible by using the respective environment assumption to model the interleaving with other threads. Finding adequate assumptions that are sufficiently precise to yield conclusive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major challenge.

In this talk, we propose a constraint-based technique for the inference of such assumptions. Our technique automatically steers towards an optimal precision/efficiency trade-off between the extremes of efficient, but incomplete thread-modular reasoning and complete, but prohibitively expensive consideration of all interleavings. We describe an application of our environment assumption inference for the verification of reachability and termination properties of multi-threaded programs, and present our experience with its implementation as well as evaluation in practice. This is joint work with Ashutosh K. Gupta and Andrey Rybalchenko.

Short bio

Corneliu Popeea is a researcher at Max Planck Institute for Software Systems in Saarbrucken. He holds a B.Sc degree (2001) from the Politehnica University of Bucharest and a Ph.D degree (2008) from the National University of Singapore. Corneliu's research interests focus on automated methods for program analysis. More specifically, he worked on inference of method pre/postconditions, type systems for object-oriented languages and thread-modular verification of concurrent programs.

© Copyright 2008-2010 ROSAEC Center, Seoul National University