Institute of Computer Languages
Compilers and Languages Group
über
| Datum: | Freitag, 10. Dezember 2010 |
|---|---|
| Zeit: | 15:00 c.t. |
| Ort: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |
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.
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.
(http://cs.uni-muenster.de/u/mmo/).
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.