Existential Label Flow Inference via CFL Reachability. Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. In Kwangkeun Yi, editor, Proceedings of the Static Analysis Symposium (SAS), volume 4134 of Lecture Notes in Computer Science, pages 88-106. Springer-Verlag, August 2006.

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(n3) 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 has been generated by bibtex2html 1.69