In programming languages, existential quantification is useful for
describing relationships among members of a structured type. For
example, we may have a list in which there *exists* some
mutual exclusion lock *l* in each list element such that *l*
protects the data stored in that element.
With this information, a static analysis can reason
about the relationship between locks and locations in the list even
when the precise identity of the lock and/or location is unknown.
To facilitate the construction of such static analyses, this paper
presents a context-sensitive *label flow analysis* algorithm with
support
for existential quantification. Label flow analysis is a core part
of many static analysis systems. Following Rehof et al, we use context-free
language (CFL) reachability to develop an efficient *O*(*n*^{3})
label flow inference algorithm. We prove the algorithm sound by reducing its
derivations to those in a system based on
polymorphically-constrained types, in the style of Mossin. We have
implemented a variant of our analysis as part of a data race detection
tool for C programs.

[ .pdf ]

@INPROCEEDINGS{pratikakis06exists, AUTHOR = {Polyvios Pratikakis and Jeffrey S. Foster and Michael Hicks}, TITLE = {Existential Label Flow Inference via {CFL} Reachability}, BOOKTITLE = {Proceedings of the Static Analysis Symposium (SAS)}, YEAR = 2006, MONTH = AUG, PUBLISHER = {Springer-Verlag}, EDITOR = {Kwangkeun Yi}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {4134}, PAGES = {88--106} }