Please use this identifier to cite or link to this item: https://doi.org/10.1145/1328408.1328434
Title: A practical and precise inference and specializer for array bound checks elimination
Authors: Popeea, C. 
Xu, D.N.
Chin, W.-N. 
Keywords: Dependent types
Safety verification
Size properties
Issue Date: 2008
Source: Popeea, C., Xu, D.N., Chin, W.-N. (2008). A practical and precise inference and specializer for array bound checks elimination. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation : 177-187. ScholarBank@NUS Repository. https://doi.org/10.1145/1328408.1328434
Abstract: Arrays are intensively used in many software programs, including those in the popular graphics and game programming domains. Although the problem of eliminating redundant array bound checks has been studied for a long time, there are few works that attempt to be both aggressively precise and practical. We propose an inference mechanism that achieves both aims by combining a forward relational analysis with a backward precondition derivation. Our inference algorithm works for a core imperative language with assignments, and analyses each method once through a summary-based approach. Our inference is precise as it is both path and context sensitive. Through a novel technique that can strengthen preconditions, we can selectively reduce the sizes of formulae to support a practical inference algorithm. Moreover, we subject each inferred program to a flexivariant specialization that can achieve good tradeoff between elimination of array checks and code explosion concerns. We have proven the soundness of our approach and have also implemented a prototype inference and specialization system. Initial experiments suggest that such a desired system is viable. Copyright © 2008 ACM.
Source Title: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
URI: http://scholarbank.nus.edu.sg/handle/10635/42038
ISBN: 9781595939777
DOI: 10.1145/1328408.1328434
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

7
checked on Dec 14, 2017

WEB OF SCIENCETM
Citations

5
checked on Nov 20, 2017

Page view(s)

46
checked on Dec 17, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.