Oct 05, 2010: Markus Müller-Olm: Lock-Join-Sensitive Analysis of Recursive Programs with Thread-Creation

October 05, 2010Lock-Join-Sensitive Analysis of Recursive Programs with Thread-Creation
Room: Zi 5126Markus Müller-Olm

We give a summary of our work on automata-based optimal analysis of programs with thread-creation and potentially recursive procedures. Specifically, we introduce dynamic pushdown networks (DPNs) that extend pushdown processes by thread creation as a model for such programs, introduce their semantics, and summarize basic results on reachability analysis and its applications. Moving from a word-shaped to tree-shaped views of executions allows us to impose regular constraints on the communicated actions in symbolic backward analysis or even to describe the entire set of executions by regular means. This in turn enables us to do lock-join-sensitive reachability analysis as the set of action trees that posses a lock-join-sensitive schedule turns out to be regular.

The talk is joint work with various people and based on papers presented at CONCUR 2005 and CAV 2009 and ongoing recent work.