Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
11-2016
Abstract
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.
Keywords
Loop Summarization, Disjunctive Summary
Discipline
OS and Networks | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 24th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Seattle, November 13-18, 2016
First Page
61
Last Page
72
ISBN
9781450342186
Identifier
10.1145/2950290.2950340
Publisher
Association for Computing Machinery
City or Country
Seattle, WA, USA
Citation
XIE, Xiaofei; CHEN, Bihuan; LIU, Yang; LE, Wei; and LI, Xiaohong.
Proteus: Computing disjunctive loop summary via path dependency analysis. (2016). Proceedings of the 24th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Seattle, November 13-18, 2016. 61-72.
Available at: https://ink.library.smu.edu.sg/sis_research/7061
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.