From Verification to Optimizations
International Workshop on Verification, Model Checking, and Abstract Interpretation: VMCAI 2015: Verification, Model Checking, and Abstract Interpretation
Compilers perform a static analysis of a program prior to optimization. The precision of this analysis is limited, however, by strict time budgets for compilation. We explore an alternative, new approach, which links external sound static analysis tools into compilers. One of the key problems to be solved is that of propagating the source-level information gathered by a static analyzer deeper into the optimization pipeline. We propose a method to achieve this, and demonstrate its feasibility through an implementation using the LLVM compiler infrastructure. We show how assertions obtained from the Frama-C source code analysis platform are propagated through LLVM and are then used to substantially improve the effectiveness of several optimizations.
Copyright © 2015, Springer
Gjomemo, Rigel; Namjoshi, Kedar S.; Phung, Phu Huu; Venkatakrishnan, V. N.; and Zuck, Lenore D., "From Verification to Optimizations" (2015). Computer Science Faculty Publications. 142.