From Verification to Optimizations

Author(s)

Rigel Gjomemo, University of Illinois at Chicago
Kedar S. Namjoshi, Nokia Bell Labs
Phu Huu Phung, University of DaytonFollow
V. N. Venkatakrishnan, University of Illinois at Chicago
Lenore D. Zuck, University of Illinois at Chicago

Document Type

Conference Paper

Publication Date

1-2015

Publication Source

International Workshop on Verification, Model Checking, and Abstract Interpretation: VMCAI 2015: Verification, Model Checking, and Abstract Interpretation

Abstract

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.

Inclusive pages

300-317

ISBN/ISSN

9783662460801

Comments

The International Workshop on Verification, Model Checking, and Abstract Interpretation: VMCAI 2015: Verification, Model Checking, and Abstract Interpretation is part of the Lecture Notes in Computer Science book series.

Permission documentation on file.

Copyright

Copyright © 2015, Springer

Publisher

Springer

Peer Reviewed

yes

eCommons Citation

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.
https://ecommons.udayton.edu/cps_fac_pub/142