Although every terminating loop has a ranking function, not every loop has a ranking function of a restricted form, such as a lexicographic tuple of polynomials over program variables. The polyranking principle is proposed as a generalization of polynomial ranking for analyzing termination of loops. We define lexicographic polyranking functions in the context of loops with parallel transitions consisting of polynomial assertions, including inequalities, over primed and unprimed variables. Next, we address synthesis of these functions with a complete and automatic method for synthesizing lexicographic linear polyranking functions with supporting linear invariants over linear loops. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bradley, A. R., Manna, Z., & Sipma, H. B. (2005). The Polyranking Principle. In Lecture Notes in Computer Science (Vol. 3580, pp. 1349–1361). Springer Verlag. https://doi.org/10.1007/11523468_109
Mendeley helps you to discover research relevant for your work.