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