Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (competition contribution). In: Workshop on Advances in Verification, pp. ĭams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions.
Ĭolóon, M.A., Sipma, H.B.: Synthesis of linear ranking functions. 53–64 (2015)Ĭolón, M.A., Sipma, H.B.: Practical methods for proving program termination.
Loopster processing software#
In: 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. Ĭhen, H., David, C., Kroening, D., Schrammel, P., Wachter, B.: Synthesising interprocedural bit-precise termination proofs (t). īraverman, M.: Termination of integer linear programs. īeyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. īen-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops.
Loopster processing verification#
Keywordsĩth competition on software verification (2020). The empirical results demonstrate the superiority of Loopster++ by achieving high accuracy of 83% in the shortest time. 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. 3) For the cycle constituted by alternate execution between paths, we classify all cycles and give the termination method of the corresponding category cycle. 2) We also propose a novel method to analyze the dependency between linear loop paths. In Loopster++, 1) we convert the iterable path into a single path linear loop to analyze its termination. To this end, we extend Loopster, named Loopster++, to analyze the termination of multi-path linear loops. But it relies on the monotonicity of variables which is very complicated to check when the variables increase. 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. 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. 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. And the termination of the loop is of great significance to the correctness of the program. collaborative applications, social network applications, and edge computing. Loop structure is widely adopted in many applications, e.g.
0 kommentar(er)
