LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures

Tuesday, June 03 2008 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Markus Müller-Olm (Westfälische Wilhelms-Universität Münster, Germany)

Most papers on precise analysis of parallel programs describe process creation by parbegin/parend blocks or their interprocedural counterpart, parallel procedure calls. In these models, the creator of processes running in parallel must wait until all the created processes have terminated before it can resume its execution. However, in presence of procedures or methods, this does not allow one to model thread creation primitives as the found in languages like Java adequately.

In this talk I am going to present recent work on fixpoint-based analysis of programs with thread creation and (recursive) procedures. Our algorithm solves gen/kill-problems precisely up to abstraction of synchronization common in this line of research; it can handle forward as well as backward problems. Our results complement earlier work on automata-based analysis of similar program models. The resulting algorithm, however, computes global information faster and more directly.

This is joint work with Peter Lammich.

About LSV