|Room||MPI-SWS, Room 112|
Verification of Concurrent Programs: Decidability, Complexity, Reductions.
Concurrency is present at different levels, from applications using high level synchronization mechanisms and abstract data structures under atomicity and isolation assumptions, to low level code implementing concurrent/distributed data structures and system services over multi-core architectures/large scale networks.
We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity: We will show the difficulties that raise in addressing this problem at the different levels mentioned above (huge amount of computations, complex control due to recursion and dynamic task creation, weak memory models, etc.), and we will overview existing approaches for tackling these issues. We will show in particular how the verification problems that must be considered in this context can be reduced to “simpler” problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already verification algorithms and tools.