基于Dixon結(jié)式和逐次差分代換的多項式秩函數(shù)探測方法

袁月 李軼

摘 要：秩函數(shù)探測是循環(huán)程序終止性分析的重要方法，目前，已有很多研究者致力于為線性循環(huán)程序探測對應(yīng)的線性秩函數(shù)，然而，針對具有多項式循環(huán)條件和多項式賦值的多項式型的循環(huán)，現(xiàn)有的秩函數(shù)探測方法還有所不足，解決方案大多是不完備的、或者具有較高的時間復(fù)雜度。針對現(xiàn)有工作對于多項式秩函數(shù)探測方法不足的問題，基于擴(kuò)展Dixon結(jié)式（KSY方法）和逐次差分代換（SDS）方法，提出一種為多項式循環(huán)程序探測多項式型秩函數(shù)的方法。首先，將待探測的秩函數(shù)模板看作帶參數(shù)系數(shù)的多項式，將秩函數(shù)的探測轉(zhuǎn)換為尋找滿足條件的參數(shù)系數(shù)的問題;然后，進(jìn)一步將問題轉(zhuǎn)換為判定相應(yīng)的方程組是否有解的問題，至此，利用KSY方法中的擴(kuò)展的Dixon結(jié)式，將問題更進(jìn)一步簡化為帶參系數(shù)多項式（即結(jié)式）嚴(yán)格為正的判定問題;最后，利用SDS方法，找到一個充分條件，使得得到的結(jié)式嚴(yán)格為正，此時，可以獲取滿足條件的參數(shù)系數(shù)的取值，從而找到一個滿足條件的秩函數(shù)，通過實驗驗證該秩函數(shù)探測方法的有效性。實驗結(jié)果表明，利用該方法，可以有效地為多項式循環(huán)程序找到多項式秩函數(shù)，包括深度為d的多階段多項式秩函數(shù)，與已有方法相比，該方法能夠更高效地找到多項式秩函數(shù)，對于基于柱形代數(shù)分解（CAD）方法的探測方法因時間復(fù)雜度問題無法而應(yīng)對的一些循環(huán)，利用所提方法能夠在幾秒內(nèi)為這些循環(huán)找到秩函數(shù)。

關(guān)鍵詞：循環(huán)程序終止性;多項式循環(huán)程序;多項式秩函數(shù);多階段秩函數(shù);Dixon結(jié)式;逐次差分代換

Abstract： Ranking function detection is one of the most important methods to analyze the termination of loop program. Some tools have been developed to detect linear ranking functions corresponding to linear loop programs. However， for polynomial loops with polynomial loop conditions and polynomial assignments， existing methods for detecting their ranking functions are mostly incomplete or with high time complexity. To deal with these weaknesses of existing work， a method was proposed for detecting polynomial ranking functions for polynomial loop programs， which was based on extended Dixon resultants （the KSY （Kapur-Saxena-Yang） method） and Successive Difference Substitution （SDS） method. Firstly， the ranking functions to be detected were seen as polynomials with parametric coefficients. Then the detection of ranking functions was transformed to the problem of finding parametric coefficients satisfying the conditions. Secondly， this problem was further transformed to the problem of determining whether the corresponding equations have solutions or not. Based on extended Dixon resultants in KSY method， the problem was reduced to the decision problem whether the polynomials with symbolic coefficients （resultants） were strictly positive or not. Thirdly， a sufficient condition making the resultants obtained strictly positive were? found by SDS method. In this way， the coefficients satisfying the conditions were able to be obtained and thus a ranking function satisfying the conditions was found. The effectiveness of the method was proved by experiments. The experimental results show that polynomial ranking functions including d-depth multi-stage polynomial ranking functions are able to be detected for polynomial loop programs. This method is more efficient to find polynomial ranking functions compared with the existing methods. For loops whose ranking functions cannot be detected by the method based on Cylindrical Algebraic Decomposition （CAD） due to high time complexity， their ranking functions are able be found within a few seconds with the proposed method.

Key words： termination of loop program; polynomial loop program; polynomial ranking function; multi-stage ranking function; Dixon resultant; Successive Difference Substitution （SDS）

0 引言

循環(huán)程序的終止性分析是程序驗證中一個重要且具有挑戰(zhàn)性的研究領(lǐng)域。對于大多數(shù)軟件來說，保證循環(huán)程序是可終止的是十分重要的。目前，已有很多出色的研究工作[1-4]基于各種計算模型來自動地進(jìn)行程序的終止性分析。秩函數(shù)法是證明循環(huán)程序終止性證明的主要方法，秩函數(shù)的存在是循環(huán)程序終止的一個充分條件。秩函數(shù)的探測在程序的正確性證明方面起著核心的作用，并且也被認(rèn)為是證明中最具挑戰(zhàn)性的一部分之一[5]。

秩函數(shù)將該循環(huán)的每個狀態(tài)映射為一個有界遞減集合中的元素，使得每當(dāng)循環(huán)完成一次迭代時，對應(yīng)的集合中的值減小。若能為一個給定的循環(huán)找到一個這種對應(yīng)的秩函數(shù)，則意味著該循環(huán)是可終止的。近來，秩函數(shù)的探測已成為一個熱門的研究方向。已有很多研究者致力于為線性循環(huán)程序探測線性秩函數(shù)，例如Colon等在2002年前后的一些早期工作[6-7]。在2004年，Podelski等[8]首次提出了一種完備有效地解決方案，基于Farkas引理[9]，為有理數(shù)域上的單分支線性循環(huán)探測線性秩函數(shù)。Ben-Amram等[10]最終在2014年，解決了針對整數(shù)域上的單分支線性循環(huán)程序的完備的線性秩函數(shù)探測方案的時間復(fù)雜度的問題。至此，從某種意義上說，如果對于一個單分支線性循環(huán)程序，存在一個對應(yīng)的線性秩函數(shù)，則一定能找到該秩函數(shù)。然而，對于一個（線性）循環(huán)程序，可能存在對應(yīng)的秩函數(shù)，卻不存在線性秩函數(shù)，并且，一般的循環(huán)程序終止性是不可判定的[11]，即使對于線性循環(huán)程序也是如此[12]。一些研究者[11，13]探測了終止性可判定的一些線性循環(huán)程序子類。Yang等[14]旨在尋找一些線性循環(huán)程序子類可終止的充分條件，使用計算機(jī)代數(shù)工具DISCOVERER來進(jìn)行輔助計算。此外，為了應(yīng)對更多的循環(huán)程序，最近一些研究者[10，15-20]構(gòu)造多個線性秩函數(shù)的組合（作為多階段秩函數(shù)）來應(yīng)對更加復(fù)雜的線性循環(huán)程序。

然而，具有線性秩函數(shù)的線性循環(huán)程序只是循環(huán)程序中的一小部分，為了捕捉更多的循環(huán)行為，一個研究方向是為具有多項式循環(huán)條件和多項式賦值語句的多項式型循環(huán)程序?qū)ふ叶囗検叫偷闹群瘮?shù)。Cousot[21]提出了一種針對半代數(shù)循環(huán)程序的多項式秩函數(shù)探測方法，他的方法基于的是拉格朗日松弛定理和半正定規(guī)劃（Semi-Definite Programming， SDP），但由于采用浮點計算，其得到秩函數(shù)并不一定是真正的秩函數(shù)，同時，拉格朗日乘子的引入也導(dǎo)致了該方法是不完備的;而Shen等[22]則在此方法的基礎(chǔ)上，利用有理恢復(fù)技術(shù)試圖找到更加精確的候選秩函數(shù)。Chen等[5]則是將探測多項式秩函數(shù)的問題轉(zhuǎn)化為了判斷半代數(shù)系統(tǒng)是否有解的問題，并基于Collins早年提出的量詞消去技術(shù)——柱形代數(shù)分解（Cylindrical Algebraic Decomposition， CAD），提出了一種完備的多項式秩函數(shù)探測方案，但由于CAD算法在糟糕情形下的復(fù)雜度是雙指數(shù)的，故限制了他們的方法只適用于較小規(guī)模的系統(tǒng)。

為了解決時間復(fù)雜度以及精確性的問題，本文提出一種為多項式循環(huán)程序探測多項式秩函數(shù)的方法，利用楊路等的研究成果，即擴(kuò)展的Dixon結(jié)式（KSY（Kapur-Saxena-Yang）方法[23]）和逐次差分代換（Successive Difference Substitution， SDS）方法[24]，來進(jìn)行秩函數(shù)的探測。具體而言，本文將循環(huán)程序的終止性證明的問題轉(zhuǎn)換為不等式的證明問題，首先，將帶探測的秩函數(shù)模板看作帶參數(shù)系數(shù)的多項式，將秩函數(shù)的探測轉(zhuǎn)換為尋找滿足條件的參數(shù)系數(shù)的問題，此時，秩函數(shù)應(yīng)當(dāng)滿足的條件被轉(zhuǎn)化為一系列帶參系數(shù)多項式不等式之間應(yīng)當(dāng)滿足一定的蘊(yùn)含關(guān)系;然后，將蘊(yùn)含關(guān)系的判定問題轉(zhuǎn)換為判定相應(yīng)的方程組是否有解的問題，至此，利用KSY方法中的擴(kuò)展的Dixon結(jié)式，將問題進(jìn)一步簡化為帶參系數(shù)多項式（即結(jié)式）嚴(yán)格為正的判定問題;最后，利用逐次差分代換（SDS）方法，找到一個充分條件，使得得到的結(jié)式嚴(yán)格為正。通過這種方式，可以獲取滿足條件的參數(shù)系數(shù)的取值，從而找到一個滿足條件的秩函數(shù)。

實驗結(jié)果表明，利用本文提出的方法可以有效地為多項式循環(huán)程序找到多項式秩函數(shù)，與現(xiàn)有基于CAD技術(shù)的完備的探測方案相比更加高效。此外，利用該方法，還能為多項式循環(huán)程序探測深度為d的多階段秩函數(shù)，更具體而言，即嵌套秩函數(shù)（2017年由Ben-Amram等[16]提出的多階段秩函數(shù)的一個更加普適性的定義）。與基于SDP方法的多項式秩函數(shù)探測方案不同的是，該方法可以找到精確的秩函數(shù)，不需要對找到的秩函數(shù)進(jìn)行再一次的驗證。

1 預(yù)備知識

本章將介紹與KSY方法和SDS方法相關(guān)的背景知識。

1.1 Dixon結(jié)式和KSY方法

給定由k+1個含k個變元的多項式方程組S：

該多項式δ則被稱為Dixon多項式。將δ看作關(guān)于α的多項式，令s′為系數(shù)個數(shù)、關(guān)于x的多項式oi（x）為每個系數(shù)，進(jìn)一步得到以下方程組：

顯然，無論α取值如何，S的任意一個解xi都是δ的一個零點，因此，xi也是多項式oi（x）的所有系數(shù)的零點，也就是說xi是方程組S′的一個解。進(jìn)一步，S′可以寫成如下形式：

其中vi（i=1，2，…，s）是δ中關(guān)于變元x1，x2，…，xk的所有冪積，D是系數(shù)矩陣。D則被稱為Dixon矩陣，而D的行列式則被稱為Dixon結(jié)式。當(dāng)s′=s時，Dixon結(jié)式有零點是原方程組S有解的一個必要條件[25]。

然而，Dixon矩陣常?？赡苁瞧娈惖?，即其行列式總等于0，或者s′≠s無法計算Dixon結(jié)式，此時，不能提供與原方程組有解相關(guān)的有用信息，因此，為了解決這個問題，Yang等[23]提出了KSY方法，來計算擴(kuò)展的Dixon結(jié)式。

令F={p1（x），p2（x），…，pk+1（x）}，給定對x的約束C，有如下形式x≠0。設(shè)Dixon矩陣的第i列為ui，它所對應(yīng)的單項式為monom（ui），令nvcol（C）為所有的滿足C monom（ui）≠0的列，而D1為所有通過刪除Dixon矩陣中屬于nvcol（C）的一列而得到s′×（s-1）的子矩陣集合。設(shè)a1，a2，…，am為m個參數(shù)，Q為有理數(shù)域的代數(shù)閉域，Φ：{a1，a2，…，am} → Q為一個映射，也就是把參數(shù)的值代入，獲取Q上的一個值，令Φ（F），Φ（D）和Φ（D1）為把參數(shù)值分別代入到F、D和D1而得到的結(jié)果，再令R={Y|Y是D的一個r×r的非奇異子矩陣}。

定理1 如果X∈D1.rank（X）此處的X，是矢量、向量或矩陣嗎？另外，rank前面（D1后面）的符號，是點還是逗號，請明確?；貜?fù)：rank前面（D1后面）的符號，是點，也就是s.t.;

根據(jù)定理1，可以得到如下的算法：先檢查是否有X∈D1.rank（X）

1.2 SDS方法

差分代換（Difference Substitution， DS）方法常被用于對稱形式的不等式的證明中，Yang[24]定義了一個更加一般的DS的概念，用于證明對稱以及非對稱形式的不等式，并且提出逐次差分替換法（即SDS方法），此后，很多研究者[26-29]對該方法進(jìn)行了進(jìn)一步的擴(kuò)展研究。利用SDS方法，可以證明多元多項式在正實數(shù)域上是半正定的。

一般地，給定一個n元多項式P，其變量x1，x2，…，xn有n！種排序結(jié)果，對諸如x1≥x2≥…≥xn的每個排序，對應(yīng)著一個替代變換：

其中，ti≥0。通過代換之后，P可以轉(zhuǎn)化為一個關(guān)于t1，t2，…，tn的多項式，而所有n！個代換得到的多項式組成的集合稱為DS。進(jìn)一步，如果該集合中的每個元素的所有系數(shù)均為非負(fù)的，則無論x1，x2，…，xn取何種非負(fù)值都有P≥0，也就是說P在正實數(shù)域上是半正定的，而如果該集合中存在一個元素有系數(shù)為負(fù)，則繼續(xù)對該多項式的DS用同樣的方式進(jìn)行檢查。以上這個過程被稱為逐次差分代換法（SDS方法）。

更進(jìn)一步，利用SDS方法，可以得到多項式P嚴(yán)格為正的一個充分條件，即如果DS中的每個元素的所有系數(shù)非負(fù)且常數(shù)項嚴(yán)格為正，則P在正實數(shù)域上是嚴(yán)格正定的。

2 不等式蘊(yùn)含關(guān)系的證明問題及其解決方法

本章將解決的是帶參數(shù)系數(shù)的多元多項式不等式蘊(yùn)含關(guān)系的證明問題，該問題定義如下。

定義1 P1。設(shè)p（x）為一個帶參數(shù)系數(shù)η1，η2，…，ηm的多項式，其中，x=（x1，x2，…，xn）T為一個含n元變量的向量。P1問題為：找到一組η1，η2，…，ηm的實數(shù)賦值，使得對任意的x∈Rn有：

證明 當(dāng)k=n時，SY為一個關(guān)于n個變元x的由n+1個多項式等式組成的方程組，又有如果H（η，ξ）≠0則SY無解，進(jìn)一步，也就是說SY無解，更進(jìn)一步，也就意味著P1問題中的關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。證畢。

注1 本文將多項式H（η，ξ）稱為式（1）在k=n的情況下的擴(kuò)展Dixon結(jié)式。在這種情況下，為解決P1問題，只需找到一個η使得H（η，ξ）在ξ∈Rk+1+上嚴(yán)格正定即可?？紤]1.2節(jié)中介紹的SDS方法，其中，需要確保DS中每一個替換后的多項式的系數(shù)非負(fù)，而對于H（η，ξ）而言，如果每個替換后的多項式的所有系數(shù)非負(fù)且常數(shù)項嚴(yán)格為正，那么則可確保H（η，ξ）在ξ∈Rk+1+上嚴(yán)格正定，也就是說，此時可以找到一組P1問題中所要尋找的η1，η2，…，ηm的賦值。

引理2 k

那么，關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。

證明 有如果H（η，，ξ）≠0則SY無解，進(jìn)一步，也就是說SY無解，更進(jìn)一步，也就意味著P1問題中的關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。證畢。

至此，只需找到一個η使得HS中的每個多項式Hi在β∈Rn+1+上嚴(yán)格正定即可。利用與注1類似的方法，可以找到一個η使得HS中的每個多項式Hi在β∈Rn+1+上嚴(yán)格正定，進(jìn)一步，也就是說，此時，H（η，，ξ）在ξ∈Rk+1+，∈Rn-k上嚴(yán)格正定，更進(jìn)一步，至此可以找到一組P1問題中所要尋找的η1，η2，…，ηm的賦值。

3 多項式秩函數(shù)探測問題

本章將介紹如何利用第2章的結(jié)果來為單路徑多項式循環(huán)程序探測多項式秩函數(shù)。首先，將給出所針對的循環(huán)程序的定義;然后，將介紹為一類循環(huán)程序探測秩函數(shù)（即深度為1的嵌套秩函數(shù)）的方法;最后將介紹為更加一般的循環(huán)程序探測深度為d的嵌套秩函數(shù)的方法。

引理3 給定一個形如式（5）的循環(huán)程序P，P在實數(shù)域上不可終止的充分必要條件是其所對應(yīng)的形如式（6）的循環(huán)程序P在實數(shù)域上不可終止。

證明 分為以下兩種情況考慮。

1）k≤b。在這種情況下，有n=b，也就是說P即為P，此時，顯然，P不可終止的充要條件為P不可終止。

2）k>b。在這種情況下，有n=k>b。

本節(jié)將針對形如式（6）的循環(huán)P的一種簡單的情況，即k=n的情況，為這類循環(huán)探測秩函數(shù)。r（x）為一個Rq → R的函數(shù)，r（x）被稱為P的秩函數(shù)，如果以下條件被滿足：

設(shè)r（x）為一個關(guān)于x的多項式，顯然，（x）=r（x）-r（M（x））-1也為一個關(guān)于x的多項式，令η=（η1，η2，…，ηq+1）T∈Rq+1為r（x）的參數(shù)系數(shù)組成的向量，η′為（x）的參數(shù)系數(shù)向量，顯然有η′=Bη，其中B是一個確定的矩陣，由循環(huán)中的賦值M和r（x）確定。

其中，η′=Bη，H1和H2分別是蘊(yùn)含式（7）和（8）的擴(kuò)展Dixon結(jié)式，則P有對應(yīng)的秩函數(shù)。

證明 已知在蘊(yùn)含式（7）和（8）中，G（x）≥0是由k個多項式不等式組成的合取式，并且x為一個含k個變量的向量，因此，根據(jù)引理1，如果存在η使得：對任意的ξ1∈Rk+1+有H1（η，ξ1）≠0并且對任意的ξ2∈Rk+1+有H2（η′，ξ2）≠0，那么式（7）對任意的x∈Rk恒成立并且對式（8）對任意的x∈Rk恒成立，此時，根據(jù)秩函數(shù)的有界和遞減的條件可知，P有對應(yīng)的秩函數(shù)r（x），該秩函數(shù)的系數(shù)由η確定。證畢。

至此，再利用類似于注1中的方法，即基于SDS方法，可以找到一個η，使得H1（η，ξ1）和H2（Bη，ξ2）對任意的ξ1∈Rk+1+和任意的ξ2∈Rk+1+均嚴(yán)格為正，此時即可找到滿足條件的秩函數(shù)。

3.3 深度為d的嵌套秩函數(shù)

多階段秩函數(shù)的概念可以進(jìn)一步擴(kuò)展為一個更一般的概念（可以應(yīng)對更多的循環(huán)程序），即嵌套秩函數(shù)[16]。接下來，將介紹為形如式（6）的循環(huán)探測深度為d的嵌套秩函數(shù)的方法。

顯然，在3.2節(jié)中定義的秩函數(shù)為一個深度為1的嵌套秩函數(shù)。

4 算法和實驗

深度為d的嵌套秩函數(shù)的探測算法如下算法1和算法2所示。在算法1中，SY指的是第3章中的式（2），Hi指的是定理3中的擴(kuò)展的Dixon結(jié)式。

算法1 DETC。帶參數(shù)系數(shù)的多元多項式不等式蘊(yùn)含關(guān)系的探測。

輸入：含d個關(guān)于n元變量的多項式的蘊(yùn)含式的合取式I（在每個蘊(yùn)含式中，前件為已知的k個多項式的合取式，后件為一個帶參系數(shù)的多項式）。

輸出：返回滿足條件的參數(shù)系數(shù)的一組賦值。

過程：

1）為每個蘊(yùn)含式中加入（k+1）個松弛變量，將I轉(zhuǎn)化為形如SY的d個多項式方程組。

2）獲取每個方程組的擴(kuò)展Dixon結(jié)式Hi（i=1，2，…，d）。

3）如果存在一組參系數(shù)賦值使得H1，H2，…，Hd均嚴(yán)格為正，則返回該賦值;否則，返回空。

算法2 探測深度為d的嵌套秩函數(shù)。

輸入：循環(huán)程序P（含n個變量，循環(huán)條件中有k個不等式，且k不大于n），秩函數(shù)模板r。

輸出：如果存在深度為d的嵌套秩函數(shù)則返回True。

過程：

1）根據(jù)秩函數(shù)需滿足的條件，將P和r轉(zhuǎn)化為含d+1個蘊(yùn)含式的合取式I;

討論 兩個算法的時間復(fù)雜度主要集中在算法1中的擴(kuò)展Dixon結(jié)式的計算以及SDS方法的計算。首先是關(guān)于Dixon結(jié)式計算的復(fù)雜度，其中主要包括構(gòu)造Dixon矩陣的復(fù)雜度（O（m21n！3∏ni=2m3i）[30]和計算Dixon結(jié)式的復(fù)雜度（即計算Dixon矩陣的行列式，O（n3n log n log log n））[31-32]。其次，關(guān)于SDS方法的計算復(fù)雜度，因為其過程是一個不可終止的過程，所以只能在給定差分代換次數(shù)上界的前提下來討論其復(fù)雜度，給定一個n元多項式，對其進(jìn)行1次差分代換，將產(chǎn)生n！個多項式，若對其進(jìn)行m次差分代換，將產(chǎn)生（n！）m個多項式。這就需要對（n！）m個多項式進(jìn)行分別處理（即從每個多項式中抽取出所有系數(shù)構(gòu)成線性不等式系統(tǒng)，然后用線性規(guī)劃工具進(jìn)行求解，這個求解過程是多項式時間復(fù)雜度的），所以，復(fù)雜度較高。盡管如此，實驗表明，對某些程序?qū)嵗?，與現(xiàn)有工具（如基于CAD的秩函數(shù)探測方法[5]）比較，本文方法能有效計算它們的秩函數(shù)。

實驗環(huán)境為：一臺處理器為Intel Core i5-6300HQ 2.3GHz、內(nèi)存為16GB、操作系統(tǒng)為64位的Windows操作系統(tǒng)的計算機(jī)，利用的是Maple 18軟件。實驗中將本文所提出的秩函數(shù)探測方法與基于CAD的秩函數(shù)探測方法[5]（利用Maple中的量消去工具RegularChains）進(jìn)行了比較，表1是實驗結(jié)果，其中循環(huán)程序10～13來自文獻(xiàn)[16，20]。實驗結(jié)果表明，利用本文提出的方法能夠更加高效地探測到秩函數(shù)（僅需用幾秒鐘的時間）。特別地，對于表1中的循環(huán)程序11，利用本文的方法也無法計算其秩函數(shù)，這是因為本文方法找到的是秩函數(shù)存在的一個充分條件，而不是充要條件。下面將給出一些例子來具體說明秩函數(shù)探測的過程。

5 結(jié)語

本文基于楊路等的研究成果，即KSY方法和SDS方法，提出了一種為多項式循環(huán)程序探測多項式秩函數(shù)的方法，給定秩函數(shù)模板，尋找滿足條件的秩函數(shù)模板中的參數(shù)，從而確定滿足條件的秩函數(shù)。實驗結(jié)果表明，對于一些多項式循環(huán)程序，可以有效地為其找到多項式秩函數(shù)（即深度為1的多階段秩函數(shù)）和深度為d的多階段秩函數(shù)。此外，與現(xiàn)有的基于SDP方法的解決方案不同，利用本文提出的方法，可以發(fā)現(xiàn)精確的秩函數(shù)，無需進(jìn)行再次驗證。本文方法能在較短時間內(nèi)為多項式循環(huán)找到對應(yīng)的多項式秩函數(shù)。在后續(xù)的工作中，本研究將針對多項式秩函數(shù)的探測問題進(jìn)行進(jìn)一步探索，以應(yīng)對更多的多項式循環(huán)程序。

參考文獻(xiàn) （References）

[1] LEIKE J， HEIZMANN M. Geometric nontermination arguments [C]// TACAS 2018： Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2018： 172-186.

[2] FEDYUKOVICH G， ZHANG Y L， GUPTA A. Syntax-guided termination analysis[C]// CAV 2018： Proceedings of the 2018 International Conference on Computer Aided Verification. Berlin： Springer， 2018： 124-143.

[3] CHEN Y F， HEIZMANN M， LENGAL O， et al. Advanced automata-based algorithms for program termination checking[C]// PLDI 2018： Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York： ACM， 2018： 135-150.

[4] LI Y. Witness to non-termination of linear programs[J]. Theoretical Computer Science， 2017， 681： 75-100.

[5] CHEN Y H， XIA B C， YANG L， et al. Discovering non-linear ranking functions by solving semi-algebraic systems[C]// ICTAC 2007： Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing. Berlin： Springer， 2007： 34-49.

[6] COLON M， SPIMA H. Synthesis of linear ranking functions[C]// TACAS 2001： Proceedings of the 2001 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2001： 67-81.

[7] COLON M， SPIMA H. Practical methods for proving program termination[C]// CAV 2002： Proceedings of the 2002 International Conference on Computer Aided Verification. Berlin： Springer， 2002： 442-454.

[8] PODELSKI A， RYBALCHENKO A. A complete method for the synthesis of linear ranking functions[C]// VMCAI 2004： Proceedings of the 2004 International Conference on Verification， Model Checking and Abstract Interpretation. Berlin： Springer， 2004： 239-251.

[9] SCHRIJVER A. Theory of Linear and Integer Programming [M]. New York： John Wiley and Sons， Inc.， 1986： 87-90.

[10] BEN-AMRAM A M， GENAIM S. Ranking functions for linear-constraint loops[J]. Journal of the ACM， 2014， 61（4）： Article No. 26.

[11] TURING A M. On computable numbers， with an application to the entscheidungs problem[J]. Proceedings of the London Mathematical Society， 1937， 42（2）： 230-265.

[12] BRAVEMAN M. Termination of integer linear programs[C]// CAV 2006： Proceedings of the 2006 International Conference on Computer Aided Verification. Berlin： Springer， 2006： 372-385.

[13] TIWARI A. Termination of linear programs[C]// CAV 2004： Proceedings of the 2004 International Conference on Computer Aided Verification. Berlin： Springer， 2004： 70-82.

[14] YANG L， ZHAN N J， XIA B C， et al. Program verification by using DISCOVERER[C]// VSTTE 2005： Proceedings of the 2005 Working Conference on Verified Software： Theories， Tools， and Experiments. Berlin： Springer， 2008： 528-538.

[15] BAGNARA R， MESNARD F. Eventual linear ranking functions[C]// PPDP 2013： Proceedings of the 2013 International Symposium on Principles and Practice of Declarative Programming. New York： ACM， 2013： 229-238.

[16] BEN-AMRAM A M， GENAIM S. On multiphase-linear ranking functions[C]// CAV 2017： Proceedings of the 2017 International Conference on Computer Aided Verification. Berlin： Springer， 2017： 601-620.

[17] BRADLEY A R， MANNA Z， SIPMA H B. Linear ranking with reachability[C]// CAV 2005： Proceedings of the 2005 International Conference on Computer Aided Verification. Berlin： Springer， 2005： 491-504.

[18] BRADLEY A R， MANNA Z， SIPMA H B. The polyranking principle[C]// ICALP 2005： Proceedings of the 2005 International Conference on Automata， Languages and Programming. Berlin： Springer， 2005： 1349-1361.

[19] LEIKE J， HEIZMANN M. Ranking templates for linear loops[C]// TACAS 2014： Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2014： 172-186.

[20] LI Y， ZHU G， FENG Y. The L-depth eventual linear ranking functions for single-path linear constraint loops[C]// TASE 2016： Proceedings of the 2016 International Symposium on Theoretical Aspects of Software Engineering. Piscataway， NJ： IEEE， 2016： 30-37.

[21] COUSOT P. Proving program invariance and termination by parametric abstraction， Lagrangian relaxation and semidefinite programming[C]// VMCAI 2005： Proceedings of the 2005 International Conference on Verification， Model Checking and Abstract Interpretation. Berlin： Springer， 2005： 1-24.

[22] SHEN L Y， WU M， YANG Z F， et al. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method[J]. Journal of Systems Science and Complexity， 2013， 26（2）： 291-301.

[23] KAPUR D， SAXENA T， YANG L. Algebraic and geometric reasoning using Dixon resultants[C]// ISSAC 1994： Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation. New York： ACM， 1994： 99-107.

[24] YANG L. Solving harder problems with lesser mathematics[C]// ATCM 2005： Proceedings of the 2005 Asian Technology Conference in Mathematics. Radford， VA： Mathematics and Technology， 2005： 37-46.

[25] DIXON A L. The eliminant of three quantics in two independent variables[J]. Proceedings of the London Mathematical Society， 1909， s2-7（49）： 49-69.

[26] 楊路，姚勇.差分代換矩陣與多項式的非負(fù)性判定[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（9）：1169-1177.（YANG L， YAO Y. Difference substitution matrices and decision on nonnegativity of polynomials [J]. Journal of Systems Science and Mathematical Sciences， 2009， 29（9）：1169-1177.）

[27] HOU X R， SHAO J W. Bounds on the number of steps of WDS required for checking the positivity of integral forms[J]. Applied Mathematics and Computation， 2011， 217（24）： 9978-9984.

[28] 韓京俊.基于差分代換的正半定型判定完備方法[J].北京大學(xué)學(xué)報（自然科學(xué)版），2013，49（4）：545-551.（HAN J J. A complete method based on successive difference substitution method for deciding positive semi-definiteness of polynomials[J]. Acta Scientiarum Naturalium Universitatis Pekinensis， 2013， 49（4）： 545-551.）

[29] 楊路.差分代換與不等式機(jī)器證明[J].廣州大學(xué)學(xué)報（自然科學(xué)版），2006，5（2）：1-7.（YANG L. Difference substitution and automated inequality proving[J]. Journal of Guangzhou University （Natural Science edition）， 2006， 5（2）： 1-7.）

[30] QIN X， WU D， TANG L， et al. Complexity of constructing Dixon resultant matrix[J]. International Journal of Computer Mathematics， 2016， 94（10）： 1-16.

[31] LI Y. An effective hybrid algorithm for computing symbolic determinants[J]. Applied Mathematics and Computation， 2009， 215（7）： 2495-2501.

[32] KALTOFEN E. On computing determinants of matrices without divisions [C]// ISSAC 1992： Proceedings of the 1992 International Symposium on Symbolic and Algebraic Computation. New York： ACM， 1992： 342-349.