We survey 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 have a lock-join-sensitive schedule turns out to be regular.

The talk is based on papers presented at CONCUR 2005, CAV 2009, and VMCAI 2011, and is a joint work with Ahmed Bouajjani, Tayssir Touili, Peter Lammich, Alexander Wenner, Thomas Gawlitza, and Helmut Seidl.

Kurzbiographie von Markus Müller-Olm:

Markus Müller-Olm studied Computer Science and Mathematics at Christian-Albrechts-Universität in Kiel, Germany, from which he got his PhD in 1996 with a dissertation on modular compiler verification.
Afterwards he has been a post-doctoral researcher at the universities of Passau, Dortmund, Trier, and Hagen. After a habilitation in 2003 at Dortmund University with a Habilitationsschrift on static analysis of
sequential and parallel programs, he is now a professor at Westfälische-Wilhelms-Universität Münster, Germany, where he heads the research group on software construction and verification.
( <link service.zid.tuwien.ac.at/ts/goto.php _blank>http://cs.uni-muenster.de/u/mmo/</link> )