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

*This file was generated by
bibtex2html 1.99.*