Loopster++: Termination Analysis for Multi-path Linear Loop

Loop structure is widely adopted in many applications, e.g. collaborative applications, social network applications, and edge computing. And the termination of the loop is of great significance to the correctness of the program. Most of the previous relative studies focused on determining the termination of a loop program by synthesizing the ranking functions, but not every ranking function can be synthesized. Although a class of linear loop program termination has been proven to be decidable, it is always difficult to analyze the termination of a multi-path linear loop. Xie et al. [20] presented Loopster to quickly check the termination of the multi-path loop program by analyzing the termination of each path and the dependency between paths. But it relies on the monotonicity of variables which is very complicated to check when the variables increase.To this end, we extend Loopster, named Loopster++, to analyze the termination of multi-path linear loops. In Loopster++, 1) we convert the iterable path into a single path linear loop to analyze its termination. 2) We also propose a novel method to analyze the dependency between linear loop paths. 3) For the cycle constituted by alternate execution between paths, we classify all cycles and give the termination method of the corresponding category cycle. We finally evaluate Loopster++ by analyzing the termination of the benchmarks from the competition on software verification and compare it with the state-of-the-art tools. The empirical results demonstrate the superiority of Loopster++ by achieving high accuracy of 83% in the shortest time.