@inbook {14693,
	title = {Existential Label Flow Inference Via CFL Reachability},
	booktitle = {Static AnalysisStatic Analysis},
	series = {Lecture Notes in Computer Science},
	volume = {4134},
	year = {2006},
	month = {2006///},
	pages = {88 - 106},
	publisher = {Springer Berlin / Heidelberg},
	organization = {Springer Berlin / Heidelberg},
	abstract = {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.},
	isbn = {978-3-540-37756-6},
	url = {http://dx.doi.org/10.1007/11823230_7},
	author = {Pratikakis,Polyvios and Foster, Jeffrey S. and Hicks, Michael W.},
	editor = {Yi,Kwangkeun}
}
