Usually, ranking function synthesis and invariant generation over a loop with integer variables involves abstracting the loop to have real variables. Integer division and modulo arithmetic must be soundly abstracted away so that the analysis over the abstracted loop is sound for the original loop. Consequently, the analysis loses precision. In contrast, we introduce a technique for handling loops over integer variables directly. The resulting analysis is more precise than previous analyses. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bradley, A. R., Manna, Z., & Sipma, H. B. (2005). Termination analysis of integer linear loops. In Lecture Notes in Computer Science (Vol. 3653, pp. 488–502). Springer Verlag. https://doi.org/10.1007/11539452_37
Mendeley helps you to discover research relevant for your work.