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.
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.