TY - GEN
T1 - Proteus
T2 - 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016
AU - Xie, Xiaofei
AU - Chen, Bihuan
AU - Liu, Yang
AU - Le, Wei
AU - Li, Xiaohong
N1 - Funding Information:
National Science Foundation of China (No. 61572349, 61272106)
Publisher Copyright:
© 2016 ACM.
PY - 2016/11/1
Y1 - 2016/11/1
N2 - Loops are challenging structures for program analysis, especially when loops contain multiple paths with complex interleaving executions among these paths. In this paper, we first propose a classification of multi-path loops to understand the complexity of the loop execution, which is based on the variable updates on the loop conditions and the execution order of the loop paths. Secondly, 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 on the variables. The key contribution is to use a path dependency automaton (PDA) to capture the execution dependency between the paths. A DFS-based algorithm is proposed to traverse the PDA to summarize the effect for all feasible executions in the loop. The experimental results show that Proteus is effective in three applications: Proteus can 1) compute a more precise bound than the existing loop bound analysis techniques; 2) significantly outperform state-of-The-Art tools for loop verification; and 3) generate test cases for deep loops within one second, while KLEE and Pex either need much more time or fail.
AB - Loops are challenging structures for program analysis, especially when loops contain multiple paths with complex interleaving executions among these paths. In this paper, we first propose a classification of multi-path loops to understand the complexity of the loop execution, which is based on the variable updates on the loop conditions and the execution order of the loop paths. Secondly, 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 on the variables. The key contribution is to use a path dependency automaton (PDA) to capture the execution dependency between the paths. A DFS-based algorithm is proposed to traverse the PDA to summarize the effect for all feasible executions in the loop. The experimental results show that Proteus is effective in three applications: Proteus can 1) compute a more precise bound than the existing loop bound analysis techniques; 2) significantly outperform state-of-The-Art tools for loop verification; and 3) generate test cases for deep loops within one second, while KLEE and Pex either need much more time or fail.
UR - http://www.scopus.com/inward/record.url?scp=84997206922&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84997206922&partnerID=8YFLogxK
U2 - 10.1145/2950290.2950340
DO - 10.1145/2950290.2950340
M3 - Conference contribution
AN - SCOPUS:84997206922
T3 - Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering
SP - 61
EP - 72
BT - FSE 2016 - Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering
A2 - Su, Zhendong
A2 - Zimmermann, Thomas
A2 - Cleland-Huang, Jane
PB - Association for Computing Machinery
Y2 - 13 November 2016 through 18 November 2016
ER -