Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/141429
Title: Automatic loop summarization via path dependency analysis
Authors: Xie, Xiaofei
Chen, Bihuan
Zou, Liang
Liu, Yang
Le, Wei
Li, Xiaohong
Keywords: Engineering::Computer science and engineering
Issue Date: 2019
Source: Xie, X., Chen, B., Zou, L., Liu, Y., Le, W., & Li, X. (2019). Automatic loop summarization via path dependency analysis. IEEE Transactions on Software Engineering, 45(6), 537 - 557. doi:10.1109/TSE.2017.2788018
Journal: IEEE Transactions on Software Engineering
Abstract: Analyzing loops is very important for various software engineering tasks such as bug detection, test case generation and program optimization. However, loops are very challenging structures for program analysis, especially when (nested) loops contain multiple paths that have complex interleaving relationships. In this paper, we propose the path dependency automaton (PDA) to capture the dependencies among the multiple paths in a loop. Based on the PDA, we first propose a loop classification to understand the complexity of loop summarization. Then, we propose a loop analysis framework, named Proteus, which takes a loop program and a set of variables of interest as inputs and summarizes path-sensitive loop effects (i.e., disjunctive loop summary) on the variables of interest. An algorithm is proposed to traverse the PDA to summarize the effect for all possible executions in the loop. We have evaluated Proteus using loops from five open-source projects and two well-known benchmarks and applying the disjunctive loop summary to three applications: loop bound analysis, program verification and test case generation. The evaluation results have demonstrated that Proteus can compute a more precise bound than the existing loop bound analysis techniques; Proteus can significantly outperform the state-of-the-art tools for loop program verification; and Proteus can help generate test cases for deep loops within one second, while symbolic execution tools KLEE and Pex either need much more time or fail.
URI: https://hdl.handle.net/10356/141429
ISSN: 0098-5589
DOI: 10.1109/TSE.2017.2788018
Rights: © 2018 IEEE. All rights reserved.
Fulltext Permission: none
Fulltext Availability: No Fulltext
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

3
Updated on Mar 2, 2021

Page view(s)

112
Updated on May 28, 2022

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.