Design and implementation of sparse global analyses for C-like languages

In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their impleme...

• Type: Journal
• Year: 2012
• Where: PLDI
• Authors: Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Kwangkeun Yi
• Keywords: Interpretation Framework, PLDI 2012, Programming Languages, Relational Semantics, Static Analyzers