Sciweavers

Share
CONCUR
2007
Springer

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

11 years 7 months ago
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
We present a fixpoint-based algorithm for context-sensitive interprocedural kill/gen-analysis of programs with thread creation. Our algorithm is precise up to abstraction of synchronization common in this line of research; it can handle forward as well as backward problems. We exploit a structural property of kill/gen-problems that allows us to analyze the influence of environment actions independently from the local transfer of data flow information. While this idea has been used for programs with parbegin/parend blocks before in work of Knoop/Steffen/Vollmer and Seidl/Steffen, considerable refinement and modification is needed to extend it to thread creation, in particular for backward problems. Our algorithm computes annotations for all program points in time depending linearly on the program size, thus being faster than a recently proposed automata based algorithm by Bouajjani et. al..
Peter Lammich, Markus Müller-Olm
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CONCUR
Authors Peter Lammich, Markus Müller-Olm
Comments (0)
books