Analyzing programs with loops is a challenging task, suffering from potential issues such as the indeterminate number of iterations and exponential growth of control flow complexity. Loop summarization based on static symbolic analysis receives increasing focus in the field of loop program analysis. However, current loop summarization methods are only suitable for single-branch loops or multi-branch loops with simple cycles and fail to handle complex multi-branch nested loops with intricate non-functional variables and irregular jumps between multiple branches. In this paper, we propose a novel loop summarization approach based on symbolic analysis to address the complex loops mentioned above and develop a tool named LoopSCC. For a non-nested loop, LoopSCC constructs an SPath Graph, where each node represents a path from entry to exit of the control flow graph of the loop and contracts it to an acyclic graph by collapsing each strongly connected component (SCC) into a single node. The summarization of a loop is the disjunction of the summaries of each path in the acyclic graph. For non-functional variables and irregular jumps, we iteratively model a valid value and refine the conditions until reaching the minimum. We introduce the oscillation interval, within which SPaths in the SCC can jump between one another. Outside this interval, no such jumps occur. This allows us to transform loop iteration transitions into a piecewise function, then summarize the interest variables according to the piecewise function. For nested loops, we construct summaries using the approaches above and apply them sequentially from the innermost loop to the outermost. Comparing state-of-the-art loop summarization tools, LoopSCC can handle more types of loops with 100% precision. We integrated LoopSCC with the symbolic execution tool, Angr, to enhance its efficiency, which enabled the detection of 18 previously unknown vulnerabilities across 11 IoT projects, 7 of which were assigned CVEs. The LoopSCC is publicly available at https://github.com/hahaleyile/LoopSCC.

@inproceedings{paperbot11804,
  title = {LoopSCC: Summarizing Complex Multi-branch Nested Loops via Periodic Oscillation Interval},
  author = {Kai Zhu and Haofeng Li and Kuihao Yan and Rongqing Wang and Jiaming Guo and Haoran Yang and Jie Lu and Lei Yu and Xiaoqi Jia and Chenkai Guo and Haichao Du and Qingjia Huang and Yamin Xie and Jing Tang},
  booktitle = {ICSE},
  year = {2026},
  doi = {10.1145/3744916.3773169}
}